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

Theorem zfrep6 5668
 Description: A version of the Axiom of Replacement. Normally would have free variables and . Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4101 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 4091. (Contributed by NM, 10-Oct-2003.)
Assertion
Ref Expression
zfrep6
Distinct variable groups:   ,   ,,,
Allowed substitution hints:   (,,)

Proof of Theorem zfrep6
StepHypRef Expression
1 euex 2139 . . . . . . 7
21ralimi 2591 . . . . . 6
3 rabid2 2690 . . . . . 6
42, 3sylibr 205 . . . . 5
5 19.42v 2039 . . . . . . 7
65abbii 2368 . . . . . 6
7 dmopab 4863 . . . . . 6
8 df-rab 2525 . . . . . 6
96, 7, 83eqtr4i 2286 . . . . 5
104, 9syl6reqr 2307 . . . 4
11 vex 2760 . . . 4
1210, 11syl6eqel 2344 . . 3
13 eumo 2156 . . . . . . 7
1413imim2i 15 . . . . . 6
15 moanimv 2174 . . . . . 6
1614, 15sylibr 205 . . . . 5
1716alimi 1546 . . . 4
18 df-ral 2521 . . . 4
19 funopab 5212 . . . 4
2017, 18, 193imtr4i 259 . . 3
21 funrnex 5667 . . 3
2212, 20, 21sylc 58 . 2
23 nfra1 2566 . . 3
2410eleq2d 2323 . . . 4
25 opabid 4229 . . . . . . . . 9
26 vex 2760 . . . . . . . . . 10
27 vex 2760 . . . . . . . . . 10
2826, 27opelrn 4884 . . . . . . . . 9
2925, 28sylbir 206 . . . . . . . 8
3029ex 425 . . . . . . 7
3130impac 607 . . . . . 6
3231eximi 1574 . . . . 5
337abeq2i 2363 . . . . 5
34 df-rex 2522 . . . . 5
3532, 33, 343imtr4i 259 . . . 4
3624, 35syl6bir 222 . . 3
3723, 36ralrimi 2597 . 2
38 nfopab1 4045 . . . . . 6
3938nfrn 4895 . . . . 5
4039nfeq2 2403 . . . 4
41 nfcv 2392 . . . . 5
42 nfopab2 4046 . . . . . 6
4342nfrn 4895 . . . . 5
4441, 43rexeqf 2706 . . . 4
4540, 44ralbid 2534 . . 3
4645cla4egv 2837 . 2
4722, 37, 46sylc 58 1
 Colors of variables: wff set class Syntax hints:   wi 6   wa 360  wal 1532  wex 1537   wceq 1619   wcel 1621  weu 2117  wmo 2118  cab 2242  wral 2516  wrex 2517  crab 2520  cvv 2757  cop 3603  copab 4036   cdm 4647   crn 4648   wfun 4653 This theorem is referenced by:  bnj865  27988 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-rep 4091  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-reu 2523  df-rab 2525  df-v 2759  df-sbc 2953  df-csb 3043  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-iun 3867  df-br 3984  df-opab 4038  df-mpt 4039  df-id 4267  df-xp 4661  df-rel 4662  df-cnv 4663  df-co 4664  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fun 4669  df-fn 4670  df-f 4671  df-f1 4672  df-fo 4673  df-f1o 4674  df-fv 4675
 Copyright terms: Public domain W3C validator