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

Theorem bnd 6195
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4805), derived from the Collection Principle cp 6194. 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 6194 . . 3 |- E.wA.x e. z (E.yph -> E.y e. w ph)
2 ralim 2230 . . . 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 1408 . . 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 1769 . 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 217 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 1380  A.wral 2169  E.wrex 2170
This theorem is referenced by:  bnd2 6196
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-13 1465  ax-14 1466  ax-17 1473  ax-9 1488  ax-4 1494  ax-16 1671  ax-ext 1942  ax-rep 3464  ax-sep 3474  ax-nul 3483  ax-pow 3519  ax-pr 3543  ax-un 3813  ax-reg 6004  ax-inf2 6039
This theorem depends on definitions:  df-bi 190  df-or 383  df-an 384  df-3or 947  df-3an 948  df-ex 1381  df-sb 1633  df-eu 1860  df-mo 1861  df-clab 1948  df-cleq 1953  df-clel 1956  df-ne 2080  df-ral 2173  df-rex 2174  df-rab 2176  df-v 2367  df-sbc 2532  df-csb 2606  df-dif 2665  df-un 2667  df-in 2669  df-ss 2671  df-pss 2673  df-nul 2927  df-if 3028  df-pw 3086  df-sn 3101  df-pr 3102  df-tp 3104  df-op 3105  df-uni 3234  df-int 3268  df-iun 3306  df-iin 3307  df-br 3379  df-opab 3433  df-tr 3448  df-eprel 3626  df-id 3629  df-po 3634  df-so 3648  df-fr 3667  df-we 3683  df-ord 3699  df-on 3700  df-lim 3701  df-suc 3702  df-om 3969  df-xp 4016  df-rel 4017  df-cnv 4018  df-co 4019  df-dm 4020  df-rn 4021  df-res 4022  df-ima 4023  df-fun 4024  df-fn 4025  df-f 4026  df-fv 4030  df-mpt 5066  df-rdg 5326  df-r1 6081  df-rank 6082
Copyright terms: Public domain