Metamath Proof Explorer


Theorem inf3lema

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 G = y V w x | w x y
inf3lem.2 F = rec G ω
inf3lem.3 A V
inf3lem.4 B V
Assertion inf3lema A G B A x A x B

Proof

Step Hyp Ref Expression
1 inf3lem.1 G = y V w x | w x y
2 inf3lem.2 F = rec G ω
3 inf3lem.3 A V
4 inf3lem.4 B V
5 ineq1 f = A f x = A x
6 5 sseq1d f = A f x B A x B
7 sseq2 v = B f x v f x B
8 7 rabbidv v = B f x | f x v = f x | f x B
9 sseq2 y = v w x y w x v
10 9 rabbidv y = v w x | w x y = w x | w x v
11 ineq1 w = f w x = f x
12 11 sseq1d w = f w x v f x v
13 12 cbvrabv w x | w x v = f x | f x v
14 10 13 eqtrdi y = v w x | w x y = f x | f x v
15 14 cbvmptv y V w x | w x y = v V f x | f x v
16 1 15 eqtri G = v V f x | f x v
17 vex x V
18 17 rabex f x | f x B V
19 8 16 18 fvmpt B V G B = f x | f x B
20 4 19 ax-mp G B = f x | f x B
21 6 20 elrab2 A G B A x A x B