Theorem bnd 6157

Description: A very strong generalization of the Axiom of Replacement (compare zfrep6 4679), derived from the Collection Principle cp 6156. 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

Proof of Theorem bnd

Step	Hyp	Ref	Expression
1		cp 6156	. . 3 |- E.wA.x e. z (E.yph -> E.y e. w ph)
2		ralim 2444	. . . 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))
3	2	eximi 1705	. . 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))
4	1, 3	ax-mp 7	. 2 |- E.w(A.x e. z E.yph -> A.x e. z E.y e. w ph)
5		19.37v 1980	. 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))
6	4, 5	mpbi 254	1 |- (A.x e. z E.yph -> E.wA.x e. z E.y e. w ph)

Syntax hints:   -> wi 3  E.wex 1644  A.wral 2385  E.wrex 2386

This theorem is referenced by:  bnd2 6158

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-reg 5972  ax-inf2 6008

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-iin 3471  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-fv 4179  df-rdg 5344  df-r1 6031  df-rank 6032

Copyright terms: Public domain