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

Theorem bnd 6249
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4807), derived from the Collection Principle cp 6248. 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 6248 . . 3
2 ralim 2200 . . . 4
32eximi 1373 . . 3
41, 3ax-mp 8 . 2
5419.37aiv 1739 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1346  wral 2138  wrex 2139
This theorem is referenced by:  bnd2 6250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-13 1433  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-rep 3448  ax-sep 3458  ax-nul 3467  ax-pow 3503  ax-pr 3527  ax-un 3799  ax-reg 6059  ax-inf2 6094
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3or 913  df-3an 914  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-rab 2145  df-v 2337  df-sbc 2502  df-csb 2579  df-dif 2641  df-un 2643  df-in 2645  df-ss 2647  df-pss 2649  df-nul 2904  df-if 3009  df-pw 3067  df-sn 3084  df-pr 3085  df-tp 3086  df-op 3087  df-uni 3218  df-int 3252  df-iun 3290  df-iin 3291  df-br 3363  df-opab 3417  df-tr 3432  df-eprel 3612  df-id 3615  df-po 3620  df-so 3634  df-fr 3653  df-we 3669  df-ord 3685  df-on 3686  df-lim 3687  df-suc 3688  df-om 3962  df-xp 4009  df-rel 4010  df-cnv 4011  df-co 4012  df-dm 4013  df-rn 4014  df-res 4015  df-ima 4016  df-fun 4017  df-fn 4018  df-f 4019  df-fv 4023  df-mpt 5070  df-rdg 5376  df-r1 6135  df-rank 6136
Copyright terms: Public domain