Metamath Proof Explorer


Theorem bnj133

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj133.1
|- ( ph <-> E. x ps )
bnj133.2
|- ( ch <-> ps )
Assertion bnj133
|- ( ph <-> E. x ch )

Proof

Step Hyp Ref Expression
1 bnj133.1
 |-  ( ph <-> E. x ps )
2 bnj133.2
 |-  ( ch <-> ps )
3 2 exbii
 |-  ( E. x ch <-> E. x ps )
4 1 3 bitr4i
 |-  ( ph <-> E. x ch )