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

Theorem bnd 6219
Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4798), derived from the Collection Principle cp 6218. 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 6218 . . 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 6220
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 3448  ax-sep 3458  ax-nul 3467  ax-pow 3503  ax-pr 3527  ax-un 3799  ax-reg 6029  ax-inf2 6064
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 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 5059  df-rdg 5349  df-r1 6105  df-rank 6106
Copyright terms: Public domain