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 nfopab1 
 |-  F/_ x { <. x , y >. | ph }
33 32 nfel2 
 |-  F/ x <. z , w >. e. { <. x , y >. | ph }
34 nfs1v 
 |-  F/ x [ z / x ] [ w / y ] ph
35 33 34 nfbi 
 |-  F/ x ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
36 opeq1 
 |-  ( x = z -> <. x , w >. = <. z , w >. )
37 36 eleq1d 
 |-  ( x = z -> ( <. x , w >. e. { <. x , y >. | ph } <-> <. z , w >. e. { <. x , y >. | ph } ) )
38 sbequ12 
 |-  ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
39 37 38 bibi12d 
 |-  ( x = z -> ( ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) <-> ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph ) ) )
40 nfopab2 
 |-  F/_ y { <. x , y >. | ph }
41 40 nfel2 
 |-  F/ y <. x , w >. e. { <. x , y >. | ph }
42 nfs1v 
 |-  F/ y [ w / y ] ph
43 41 42 nfbi 
 |-  F/ y ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
44 opeq2 
 |-  ( y = w -> <. x , y >. = <. x , w >. )
45 44 eleq1d 
 |-  ( y = w -> ( <. x , y >. e. { <. x , y >. | ph } <-> <. x , w >. e. { <. x , y >. | ph } ) )
46 sbequ12 
 |-  ( y = w -> ( ph <-> [ w / y ] ph ) )
47 45 46 bibi12d 
 |-  ( y = w -> ( ( <. x , y >. e. { <. x , y >. | ph } <-> ph ) <-> ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph ) ) )
48 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
49 43 47 48 chvarfv 
 |-  ( <. x , w >. e. { <. x , y >. | ph } <-> [ w / y ] ph )
50 35 39 49 chvarfv 
 |-  ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
51 26 31 50 vtocl2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph ) )
52 16 22 51 pm5.21nii 
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )