Theorem elabed1 ≪ | index | src | ≫

theorem elabed1 (A: set) (G P: wff) (a: nat) {x: nat} (p: wff x):
  $ G /\ x = a -> (a e. A <-> p) -> P $ >
  $ G -> A == {x | p} -> P $;

Step	Hyp	Ref	Expression
1		ax_6	E. x x = a
2		nfv	F/ x G
3		nfsv	FS/ x A
4		nfab1	FS/ x {x \| p}
5	3, 4	nfeqs	F/ x A == {x \| p}
6		nfv	F/ x P
7	5, 6	nfim	F/ x A == {x \| p} -> P
8		eleq2	A == {x \| p} -> (a e. A <-> a e. {x \| p})
9	8	bieq1d	A == {x \| p} -> (a e. A <-> p <-> (a e. {x \| p} <-> p))
10		anr	G /\ x = a -> x = a
11	10	eleq1d	G /\ x = a -> (x e. {x \| p} <-> a e. {x \| p})
12		abid	x e. {x \| p} <-> p
13	12	a1i	G /\ x = a -> (x e. {x \| p} <-> p)
14	11, 13	bitr3d	G /\ x = a -> (a e. {x \| p} <-> p)
15	9, 14	syl5ibrcom	G /\ x = a -> A == {x \| p} -> (a e. A <-> p)
16		hyp e	G /\ x = a -> (a e. A <-> p) -> P
17	15, 16	syld	G /\ x = a -> A == {x \| p} -> P
18	17	exp	G -> x = a -> A == {x \| p} -> P
19	2, 7, 18	eexdh	G -> E. x x = a -> A == {x \| p} -> P
20	1, 19	mpi	G -> A == {x \| p} -> P

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)