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

Theorem bnd 6815
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 5053), derived from the Collection Principle cp 6814. 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 6814 . . 3
2 ralim 2301 . . . 4
32eximi 1474 . . 3
41, 3ax-mp 8 . 2
5419.37aiv 1840 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1447  wral 2239  wrex 2240
This theorem is referenced by:  bnd2 6816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-13 1534  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-rep 3616  ax-sep 3626  ax-nul 3635  ax-pow 3671  ax-pr 3695  ax-un 3973  ax-reg 6572  ax-inf2 6607
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3or 900  df-3an 901  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-rab 2246  df-v 2442  df-sbc 2609  df-csb 2691  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-pss 2763  df-nul 3026  df-if 3135  df-pw 3196  df-sn 3214  df-pr 3215  df-tp 3216  df-op 3217  df-uni 3375  df-int 3409  df-iun 3451  df-iin 3452  df-br 3532  df-opab 3585  df-tr 3600  df-eprel 3783  df-id 3787  df-po 3792  df-so 3806  df-fr 3826  df-we 3842  df-ord 3858  df-on 3859  df-lim 3860  df-suc 3861  df-om 4139  df-xp 4186  df-rel 4187  df-cnv 4188  df-co 4189  df-dm 4190  df-rn 4191  df-res 4192  df-ima 4193  df-fun 4194  df-fn 4195  df-f 4196  df-fv 4200  df-mpt 5371  df-recs 5722  df-rdg 5750  df-r1 6701  df-rank 6702
Copyright terms: Public domain