Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axrep3 Unicode version

Theorem axrep3 4135
 Description: Axiom of Replacement slightly strengthened from axrep2 4134; may occur free in . (Contributed by NM, 2-Jan-1997.)
Assertion
Ref Expression
axrep3
Distinct variable group:   ,,,
Allowed substitution hints:   (,,,)

Proof of Theorem axrep3
StepHypRef Expression
1 nfe1 1707 . . . 4
2 nfv 1606 . . . . . 6
3 nfv 1606 . . . . . . . 8
4 nfa1 1757 . . . . . . . 8
53, 4nfan 1772 . . . . . . 7
65nfex 1768 . . . . . 6
72, 6nfbi 1773 . . . . 5
87nfal 1767 . . . 4
91, 8nfim 1770 . . 3
109nfex 1768 . 2
11 elequ2 1690 . . . . . . . 8
1211anbi1d 687 . . . . . . 7
1312exbidv 1613 . . . . . 6
1413bibi2d 311 . . . . 5
1514albidv 1612 . . . 4
1615imbi2d 309 . . 3
1716exbidv 1613 . 2
18 axrep2 4134 . 2
1910, 17, 18chvar 1928 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wa 360  wal 1528  wex 1529   wceq 1624   wcel 1685 This theorem is referenced by:  axrep4  4136 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-rep 4132 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-cleq 2277  df-clel 2280
 Copyright terms: Public domain W3C validator