This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ceqsrexbv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Hypothesis ceqsrexv.1 
|- ( x = A -> ( ph <-> ps ) )
Assertion ceqsrexbv 
|- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) )

Proof

Step Hyp Ref Expression
1 ceqsrexv.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 r19.42v 
 |-  ( E. x e. B ( A e. B /\ ( x = A /\ ph ) ) <-> ( A e. B /\ E. x e. B ( x = A /\ ph ) ) )
3 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
4 3 adantr 
 |-  ( ( x = A /\ ph ) -> ( x e. B <-> A e. B ) )
5 4 pm5.32ri 
 |-  ( ( x e. B /\ ( x = A /\ ph ) ) <-> ( A e. B /\ ( x = A /\ ph ) ) )
6 5 bicomi 
 |-  ( ( A e. B /\ ( x = A /\ ph ) ) <-> ( x e. B /\ ( x = A /\ ph ) ) )
7 6 baib 
 |-  ( x e. B -> ( ( A e. B /\ ( x = A /\ ph ) ) <-> ( x = A /\ ph ) ) )
8 7 rexbiia 
 |-  ( E. x e. B ( A e. B /\ ( x = A /\ ph ) ) <-> E. x e. B ( x = A /\ ph ) )
9 1 ceqsrexv 
 |-  ( A e. B -> ( E. x e. B ( x = A /\ ph ) <-> ps ) )
10 9 pm5.32i 
 |-  ( ( A e. B /\ E. x e. B ( x = A /\ ph ) ) <-> ( A e. B /\ ps ) )
11 2 8 10 3bitr3i 
 |-  ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) )