HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem 2rexbidv 1678
Description: Formula-building rule for restricted existential quantifiers (deduction rule).
Hypothesis
Ref Expression
2ralbidv.1 |- (ph -> (ps <-> ch))
Assertion
Ref Expression
2rexbidv |- (ph -> (E.x e. A E.y e. B ps <-> E.x e. A E.y e. B ch))
Distinct variable groups:   ph,x   ph,y
Proof of Theorem 2rexbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 |- (ph -> (ps <-> ch))
21rexbidv 1661 . 2 |- (ph -> (E.y e. B ps <-> E.y e. B ch))
32rexbidv 1661 1 |- (ph -> (E.x e. A E.y e. B ps <-> E.x e. A E.y e. B ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146  E.wrex 1643
This theorem is referenced by:  f1oiso 3895  oprvalelrn 4030  brdom7disj 4784  brdom6disj 4785  axcnre 5266  elq 6203  hausnei 7734  pjtht 9172  shselt 9216  iseuctopg 10425
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647
Copyright terms: Public domain