Theorem axrep2 4565

Description: Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on . (Contributed by NM, 15-Aug-2003.)

Assertion

Ref	Expression
axrep2

Distinct variable group:   ,,

Proof of Theorem axrep2

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfe1 1840	. . . . 5
2		nfv 1707	. . . . 5
3	1, 2	nfim 1920	. . . 4
4	3	nfex 1948	. . 3
5		elequ2 1823	. . . . . . . . 9
6	5	anbi1d 704	. . . . . . . 8
7	6	exbidv 1714	. . . . . . 7
8	7	bibi2d 318	. . . . . 6
9	8	albidv 1713	. . . . 5
10	9	imbi2d 316	. . . 4
11	10	exbidv 1714	. . 3
12		axrep1 4564	. . 3
13	4, 11, 12	chvar 2013	. 2
14		sp 1859	. . . . . . 7
15	14	imim1i 58	. . . . . 6
16	15	alimi 1633	. . . . 5
17	16	eximi 1656	. . . 4
18		nfv 1707	. . . . 5
19		nfa1 1897	. . . . . . 7
20		nfv 1707	. . . . . . 7
21	19, 20	nfim 1920	. . . . . 6
22	21	nfal 1947	. . . . 5
23		equequ2 1799	. . . . . . 7
24	23	imbi2d 316	. . . . . 6
25	24	albidv 1713	. . . . 5
26	18, 22, 25	cbvex 2022	. . . 4
27	17, 26	sylib 196	. . 3
28	27	imim1i 58	. 2
29	13, 28	eximii 1658	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612

This theorem is referenced by:  axrep3  4566  axrepndlem1  8988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-rep 4563

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617