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

Metamath Proof Explorer

Theorem prtlem100

Description: Lemma for prter3 . (Contributed by Rodolfo Medina, 19-Oct-2010)

Ref Expression
Assertion prtlem100 
|- ( E. x e. A ( B e. x /\ ph ) <-> E. x e. ( A \ { (/) } ) ( B e. x /\ ph ) )

Proof

Step Hyp Ref Expression
1 anass 
 |-  ( ( ( x e. A /\ x =/= (/) ) /\ ( B e. x /\ ph ) ) <-> ( x e. A /\ ( x =/= (/) /\ ( B e. x /\ ph ) ) ) )
2 eldifsn 
 |-  ( x e. ( A \ { (/) } ) <-> ( x e. A /\ x =/= (/) ) )
3 2 anbi1i 
 |-  ( ( x e. ( A \ { (/) } ) /\ ( B e. x /\ ph ) ) <-> ( ( x e. A /\ x =/= (/) ) /\ ( B e. x /\ ph ) ) )
4 ne0i 
 |-  ( B e. x -> x =/= (/) )
5 4 pm4.71ri 
 |-  ( B e. x <-> ( x =/= (/) /\ B e. x ) )
6 5 anbi1i 
 |-  ( ( B e. x /\ ph ) <-> ( ( x =/= (/) /\ B e. x ) /\ ph ) )
7 anass 
 |-  ( ( ( x =/= (/) /\ B e. x ) /\ ph ) <-> ( x =/= (/) /\ ( B e. x /\ ph ) ) )
8 6 7 bitri 
 |-  ( ( B e. x /\ ph ) <-> ( x =/= (/) /\ ( B e. x /\ ph ) ) )
9 8 anbi2i 
 |-  ( ( x e. A /\ ( B e. x /\ ph ) ) <-> ( x e. A /\ ( x =/= (/) /\ ( B e. x /\ ph ) ) ) )
10 1 3 9 3bitr4ri 
 |-  ( ( x e. A /\ ( B e. x /\ ph ) ) <-> ( x e. ( A \ { (/) } ) /\ ( B e. x /\ ph ) ) )
11 10 rexbii2 
 |-  ( E. x e. A ( B e. x /\ ph ) <-> E. x e. ( A \ { (/) } ) ( B e. x /\ ph ) )