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

Theorem bnd 6234
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4803), derived from the Collection Principle cp 6233. Its strength lies in the rather profound fact that ph(x, y) 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 |- (A.x e. z E.yph -> E.wA.x e. z E.y e. w ph)
Distinct variable groups:   ph,z,w   x,y,z,w
Allowed substitution hints:   ph(x,y)

Proof of Theorem bnd
StepHypRef Expression
1 cp 6233 . . 3 |- E.wA.x e. z (E.yph -> E.y e. w ph)
2 ralim 2208 . . . 4 |- (A.x e. z (E.yph -> E.y e. w ph) -> (A.x e. z E.yph -> A.x e. z E.y e. w ph))
32eximi 1382 . . 3 |- (E.wA.x e. z (E.yph -> E.y e. w ph) -> E.w(A.x e. z E.yph -> A.x e. z E.y e. w ph))
41, 3ax-mp 8 . 2 |- E.w(A.x e. z E.yph -> A.x e. z E.y e. w ph)
5419.37aiv 1748 1 |- (A.x e. z E.yph -> E.wA.x e. z E.y e. w ph)
Colors of variables: wff set class
Syntax hints:   -> wi 4  E.wex 1355  A.wral 2147  E.wrex 2148
This theorem is referenced by:  bnd2 6235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-13 1442  ax-14 1443  ax-17 1450  ax-9 1465  ax-4 1471  ax-16 1649  ax-ext 1920  ax-rep 3449  ax-sep 3459  ax-nul 3468  ax-pow 3504  ax-pr 3528  ax-un 3800  ax-reg 6044  ax-inf2 6079
This theorem depends on definitions:  df-bi 175  df-or 362  df-an 363  df-3or 922  df-3an 923  df-ex 1356  df-sb 1611  df-eu 1838  df-mo 1839  df-clab 1926  df-cleq 1931  df-clel 1934  df-ne 2058  df-ral 2151  df-rex 2152  df-rab 2154  df-v 2345  df-sbc 2510  df-csb 2585  df-dif 2645  df-un 2647  df-in 2649  df-ss 2651  df-pss 2653  df-nul 2907  df-if 3010  df-pw 3068  df-sn 3085  df-pr 3086  df-tp 3087  df-op 3088  df-uni 3219  df-int 3253  df-iun 3291  df-iin 3292  df-br 3364  df-opab 3418  df-tr 3433  df-eprel 3613  df-id 3616  df-po 3621  df-so 3635  df-fr 3654  df-we 3670  df-ord 3686  df-on 3687  df-lim 3688  df-suc 3689  df-om 3963  df-xp 4010  df-rel 4011  df-cnv 4012  df-co 4013  df-dm 4014  df-rn 4015  df-res 4016  df-ima 4017  df-fun 4018  df-fn 4019  df-f 4020  df-fv 4024  df-mpt 5065  df-rdg 5364  df-r1 6120  df-rank 6121
Copyright terms: Public domain