Metamath Proof Explorer

Theorem opelopabsb

Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002) (Revised by Mario Carneiro, 18-Nov-2016)

Ref Expression
Assertion opelopabsb 
|- ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 vex 
 |-  y e. _V
3 1 2 opnzi 
 |-  <. x , y >. =/= (/)
4 simpl 
 |-  ( ( (/) = <. x , y >. /\ ph ) -> (/) = <. x , y >. )
5 4 eqcomd 
 |-  ( ( (/) = <. x , y >. /\ ph ) -> <. x , y >. = (/) )
6 5 necon3ai 
 |-  ( <. x , y >. =/= (/) -> -. ( (/) = <. x , y >. /\ ph ) )
7 3 6 ax-mp 
 |-  -. ( (/) = <. x , y >. /\ ph )
8 7 nex 
 |-  -. E. y ( (/) = <. x , y >. /\ ph )
9 8 nex 
 |-  -. E. x E. y ( (/) = <. x , y >. /\ ph )
10 elopab 
 |-  ( (/) e. { <. x , y >. | ph } <-> E. x E. y ( (/) = <. x , y >. /\ ph ) )
11 9 10 mtbir 
 |-  -. (/) e. { <. x , y >. | ph }
12 eleq1 
 |-  ( <. A , B >. = (/) -> ( <. A , B >. e. { <. x , y >. | ph } <-> (/) e. { <. x , y >. | ph } ) )
13 11 12 mtbiri 
 |-  ( <. A , B >. = (/) -> -. <. A , B >. e. { <. x , y >. | ph } )
14 13 necon2ai 
 |-  ( <. A , B >. e. { <. x , y >. | ph } -> <. A , B >. =/= (/) )
15 opnz 
 |-  ( <. A , B >. =/= (/) <-> ( A e. _V /\ B e. _V ) )
16 14 15 sylib 
 |-  ( <. A , B >. e. { <. x , y >. | ph } -> ( A e. _V /\ B e. _V ) )
17 sbcex 
 |-  ( [. A / x ]. [. B / y ]. ph -> A e. _V )
18 spesbc 
 |-  ( [. A / x ]. [. B / y ]. ph -> E. x [. B / y ]. ph )
19 sbcex 
 |-  ( [. B / y ]. ph -> B e. _V )
20 19 exlimiv 
 |-  ( E. x [. B / y ]. ph -> B e. _V )
21 18 20 syl 
 |-  ( [. A / x ]. [. B / y ]. ph -> B e. _V )
22 17 21 jca 
 |-  ( [. A / x ]. [. B / y ]. ph -> ( A e. _V /\ B e. _V ) )
23 opeq1 
 |-  ( z = A -> <. z , w >. = <. A , w >. )
24 23 eleq1d 
 |-  ( z = A -> ( <. z , w >. e. { <. x , y >. | ph } <-> <. A , w >. e. { <. x , y >. | ph } ) )
25 dfsbcq2 
 |-  ( z = A -> ( [ z / x ] [ w / y ] ph <-> [. A / x ]. [ w / y ] ph ) )
26 24 25 bibi12d 
 |-  ( z = A -> ( ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph ) <-> ( <. A , w >. e. { <. x , y >. | ph } <-> [. A / x ]. [ w / y ] ph ) ) )
27 opeq2 
 |-  ( w = B -> <. A , w >. = <. A , B >. )
28 27 eleq1d 
 |-  ( w = B -> ( <. A , w >. e. { <. x , y >. | ph } <-> <. A , B >. e. { <. x , y >. | ph } ) )
29 dfsbcq2 
 |-  ( w = B -> ( [ w / y ] ph <-> [. B / y ]. ph ) )
30 29 sbcbidv 
 |-  ( w = B -> ( [. A / x ]. [ w / y ] ph <-> [. A / x ]. [. B / y ]. ph ) )
31 28 30 bibi12d 
 |-  ( w = B -> ( ( <. A , w >. e. { <. x , y >. | ph } <-> [. A / x ]. [ w / y ] ph ) <-> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) ) )
32 vopelopabsb 
 |-  ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
33 26 31 32 vtocl2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
34 16 22 33 pm5.21nii 
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )