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=yVwx|wxy
inf3lem.2 F=recGω
inf3lem.3 AV
inf3lem.4 BV
Assertion inf3lemb F=

Proof

Step Hyp Ref Expression
1 inf3lem.1 G=yVwx|wxy
2 inf3lem.2 F=recGω
3 inf3lem.3 AV
4 inf3lem.4 BV
5 2 fveq1i F=recGω
6 0ex V
7 fr0g VrecGω=
8 6 7 ax-mp recGω=
9 5 8 eqtri F=