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

Theorem bnd 6974
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 5135), derived from the Collection Principle cp 6973. Its strength lies in the rather profound fact that does not have to be a "function-like" wff, as it does in the standard Axiom of Replacement. This theorem is sometimes called the Boundedness Axiom.
Assertion
Ref Expression
bnd
Distinct variable groups:   ,,   ,,,
Allowed substitution hints:   (,)

Proof of Theorem bnd
StepHypRef Expression
1 cp 6973 . . 3
2 ralim 2361 . . . 4
32eximi 1479 . . 3
41, 3ax-mp 8 . 2
5419.37aiv 1893 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1450  wral 2299  wrex 2300
This theorem is referenced by:  bnd2  6975
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