Theorem axrep1 4564

Description: The version of the Axiom of Replacement used in the Metamath Solitaire applet http://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 4563 -> axrep1 4564 -> axrep2 4565 -> axrepnd 8990 -> zfcndrep 9013 = ax-rep 4563. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.)

Assertion

Ref	Expression
axrep1

Distinct variable groups:   ,   ,,

Proof of Theorem axrep1

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ2 1823	. . . . . . . . 9
2	1	anbi1d 704	. . . . . . . 8
3	2	exbidv 1714	. . . . . . 7
4	3	bibi2d 318	. . . . . 6
5	4	albidv 1713	. . . . 5
6	5	exbidv 1714	. . . 4
7	6	imbi2d 316	. . 3
8		ax-rep 4563	. . . 4
9		19.3v 1755	. . . . . . . 8
10	9	imbi1i 325	. . . . . . 7
11	10	albii 1640	. . . . . 6
12	11	exbii 1667	. . . . 5
13	12	albii 1640	. . . 4
14		nfv 1707	. . . . . . 7
15		nfe1 1840	. . . . . . 7
16	14, 15	nfbi 1934	. . . . . 6
17	16	nfal 1947	. . . . 5
18		nfv 1707	. . . . 5
19		elequ2 1823	. . . . . . 7
20	9	anbi2i 694	. . . . . . . . 9
21	20	exbii 1667	. . . . . . . 8
22	21	a1i 11	. . . . . . 7
23	19, 22	bibi12d 321	. . . . . 6
24	23	albidv 1713	. . . . 5
25	17, 18, 24	cbvex 2022	. . . 4
26	8, 13, 25	3imtr3i 265	. . 3
27	7, 26	chvarv 2014	. 2
28	27	19.35ri 1690	1

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

This theorem is referenced by:  axrep2  4565

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