Metamath Proof Explorer


Theorem inf3lemb

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 inf3lemb F =

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 2 fveq1i F = rec G ω
6 0ex V
7 fr0g V rec G ω =
8 6 7 ax-mp rec G ω =
9 5 8 eqtri F =