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

Theorem bnd 6335
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4939), derived from the Collection Principle cp 6334. 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 6334 . . 3 |- E.wA.x e. z (E.yph -> E.y e. w ph)
2 ralim 2369 . . . 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 1547 . . 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 7 . 2 |- E.w(A.x e. z E.yph -> A.x e. z E.y e. w ph)
5 19.37v 1901 . 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 237 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 3  E.wex 1520  A.wral 2310  E.wrex 2311
This theorem is referenced by:  bnd2 6336
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-13 1600  ax-14 1601  ax-17 1608  ax-9 1620  ax-4 1626  ax-16 1803  ax-ext 2074  ax-rep 3599  ax-sep 3609  ax-nul 3619  ax-pow 3655  ax-pr 3679  ax-un 3947  ax-reg 6102  ax-inf2 6137
This theorem depends on definitions:  df-bi 210  df-or 419  df-an 420  df-3or 1038  df-3an 1039  df-ex 1521  df-sb 1765  df-eu 1992  df-mo 1993  df-clab 2080  df-cleq 2085  df-clel 2088  df-ne 2220  df-ral 2314  df-rex 2315  df-rab 2317  df-v 2501  df-sbc 2671  df-csb 2745  df-dif 2804  df-un 2806  df-in 2808  df-ss 2810  df-pss 2812  df-nul 3066  df-if 3166  df-pw 3222  df-sn 3237  df-pr 3238  df-tp 3240  df-op 3241  df-uni 3365  df-int 3399  df-iun 3437  df-iin 3438  df-br 3510  df-opab 3568  df-tr 3583  df-eprel 3762  df-id 3765  df-po 3770  df-so 3782  df-fr 3800  df-we 3816  df-ord 3832  df-on 3833  df-lim 3834  df-suc 3835  df-om 4104  df-xp 4151  df-rel 4152  df-cnv 4153  df-co 4154  df-dm 4155  df-rn 4156  df-res 4157  df-ima 4158  df-fun 4159  df-fn 4160  df-f 4161  df-fv 4165  df-mpt 5202  df-rdg 5460  df-r1 6182  df-rank 6183
Copyright terms: Public domain