Metamath Proof Explorer

Theorem elex22VD

Description: Virtual deduction proof of elex22 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elex22VD 
|- ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) )

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. ( A e. B /\ A e. C ) ->. ( A e. B /\ A e. C ) ).
2 simpl 
 |-  ( ( A e. B /\ A e. C ) -> A e. B )
3 1 2 e1a 
 |-  (. ( A e. B /\ A e. C ) ->. A e. B ).
4 elisset 
 |-  ( A e. B -> E. x x = A )
5 3 4 e1a 
 |-  (. ( A e. B /\ A e. C ) ->. E. x x = A ).
6 idn2 
 |-  (. ( A e. B /\ A e. C ) ,. x = A ->. x = A ).
7 eleq1a 
 |-  ( A e. B -> ( x = A -> x e. B ) )
8 3 6 7 e12 
 |-  (. ( A e. B /\ A e. C ) ,. x = A ->. x e. B ).
9 simpr 
 |-  ( ( A e. B /\ A e. C ) -> A e. C )
10 1 9 e1a 
 |-  (. ( A e. B /\ A e. C ) ->. A e. C ).
11 eleq1a 
 |-  ( A e. C -> ( x = A -> x e. C ) )
12 10 6 11 e12 
 |-  (. ( A e. B /\ A e. C ) ,. x = A ->. x e. C ).
13 pm3.2 
 |-  ( x e. B -> ( x e. C -> ( x e. B /\ x e. C ) ) )
14 8 12 13 e22 
 |-  (. ( A e. B /\ A e. C ) ,. x = A ->. ( x e. B /\ x e. C ) ).
15 14 in2 
 |-  (. ( A e. B /\ A e. C ) ->. ( x = A -> ( x e. B /\ x e. C ) ) ).
16 15 gen11 
 |-  (. ( A e. B /\ A e. C ) ->. A. x ( x = A -> ( x e. B /\ x e. C ) ) ).
17 exim 
 |-  ( A. x ( x = A -> ( x e. B /\ x e. C ) ) -> ( E. x x = A -> E. x ( x e. B /\ x e. C ) ) )
18 16 17 e1a 
 |-  (. ( A e. B /\ A e. C ) ->. ( E. x x = A -> E. x ( x e. B /\ x e. C ) ) ).
19 pm2.27 
 |-  ( E. x x = A -> ( ( E. x x = A -> E. x ( x e. B /\ x e. C ) ) -> E. x ( x e. B /\ x e. C ) ) )
20 5 18 19 e11 
 |-  (. ( A e. B /\ A e. C ) ->. E. x ( x e. B /\ x e. C ) ).
21 20 in1 
 |-  ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) )