HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem cp 6973
Description: Collection Principle. This remarkable theorem scheme is in effect a very strong generalization of the Axiom of Replacement. The proof makes use of Scott's trick scottex 6967 that collapses a proper class into a set of minimum rank. The wff can be thought of as . Scheme "Collection Principle" of [Jech] p. 72.
Assertion
Ref Expression
cp
Distinct variable groups:   ,,   ,,,
Allowed substitution hints:   (,)

Proof of Theorem cp
StepHypRef Expression
1 vex 2503 . . 3
21cplem2 6972 . 2
3 abn0 3103 . . . . 5
4 elin 2993 . . . . . . . 8
5 abid 2079 . . . . . . . . 9
65anbi1i 672 . . . . . . . 8
7 ancom 430 . . . . . . . 8
84, 6, 73bitri 260 . . . . . . 7
98exbii 1486 . . . . . 6
10 hbab1 2080 . . . . . . . 8
11 ax-17 1542 . . . . . . . 8
1210, 11hbin 3009 . . . . . . 7
1312n0f 3093 . . . . . 6
14 df-rex 2304 . . . . . 6
159, 13, 143bitr4i 266 . . . . 5
163, 15imbi12i 314 . . . 4
1716ralbii 2321 . . 3
1817exbii 1486 . 2
192, 18mpbi 197 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357  wex 1450   wcel 1533  cab 2077   wne 2207  wral 2299  wrex 2300   cin 2809  c0 3085
This theorem is referenced by:  bnd  6974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-13 1538  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-rep 3677  ax-sep 3687  ax-nul 3696  ax-pow 3732  ax-pr 3756  ax-un 4049  ax-reg 6719  ax-inf2 6755
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-reu 2305  df-rab 2306  df-v 2502  df-sbc 2669  df-csb 2751  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-pss 2823  df-nul 3086  df-if 3195  df-pw 3256  df-sn 3274  df-pr 3275  df-tp 3276  df-op 3277  df-uni 3435  df-int 3469  df-iun 3511  df-iin 3512  df-br 3592  df-opab 3645  df-tr 3660  df-eprel 3844  df-id 3848  df-po 3853  df-so 3854  df-fr 3891  df-we 3893  df-ord 3934  df-on 3935  df-lim 3936  df-suc 3937  df-om 4216  df-xp 4263  df-rel 4264  df-cnv 4265  df-co 4266  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fun 4271  df-fn 4272  df-f 4273  df-f1 4274  df-fo 4275  df-f1o 4276  df-fv 4277  df-mpt 5461  df-recs 5814  df-rdg 5849  df-r1 6849  df-rank 6850
Copyright terms: Public domain