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

Theorem bnd 6227
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4807), derived from the Collection Principle cp 6226. 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 6226 . . 3 |- E.wA.x e. z (E.yph -> E.y e. w ph)
2 ralim 2223 . . . 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 1399 . . 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)
5 19.37v 1762 . 2 |- (E.w(A.x e. z E.yph -> A.x e. z E.y e. w ph) <-> (A.x e. z E.yph -> E.wA.x e. z E.y e. w ph))
64, 5mpbi 212 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 1371  A.wral 2162  E.wrex 2163
This theorem is referenced by:  bnd2 6228
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-13 1457  ax-14 1458  ax-17 1465  ax-9 1480  ax-4 1486  ax-16 1664  ax-ext 1935  ax-rep 3459  ax-sep 3469  ax-nul 3478  ax-pow 3514  ax-pr 3538  ax-un 3808  ax-reg 6036  ax-inf2 6071
This theorem depends on definitions:  df-bi 185  df-or 378  df-an 379  df-3or 938  df-3an 939  df-ex 1372  df-sb 1626  df-eu 1853  df-mo 1854  df-clab 1941  df-cleq 1946  df-clel 1949  df-ne 2073  df-ral 2166  df-rex 2167  df-rab 2169  df-v 2360  df-sbc 2525  df-csb 2600  df-dif 2660  df-un 2662  df-in 2664  df-ss 2666  df-pss 2668  df-nul 2922  df-if 3023  df-pw 3081  df-sn 3096  df-pr 3097  df-tp 3099  df-op 3100  df-uni 3229  df-int 3263  df-iun 3301  df-iin 3302  df-br 3374  df-opab 3428  df-tr 3443  df-eprel 3621  df-id 3624  df-po 3629  df-so 3643  df-fr 3662  df-we 3678  df-ord 3694  df-on 3695  df-lim 3696  df-suc 3697  df-om 3971  df-xp 4018  df-rel 4019  df-cnv 4020  df-co 4021  df-dm 4022  df-rn 4023  df-res 4024  df-ima 4025  df-fun 4026  df-fn 4027  df-f 4028  df-fv 4032  df-mpt 5068  df-rdg 5356  df-r1 6113  df-rank 6114
Copyright terms: Public domain