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

Metamath Proof Explorer

Theorem vopelopabsb

Description: The law of concretion in terms of substitutions. Version of opelopabsb with set variables. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) Remove unnecessary commutation. (Revised by SN, 1-Sep-2024)

Ref Expression
Assertion vopelopabsb 
|- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )

Proof

Step Hyp Ref Expression
1 eqcom 
 |-  ( <. z , w >. = <. x , y >. <-> <. x , y >. = <. z , w >. )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 opth 
 |-  ( <. x , y >. = <. z , w >. <-> ( x = z /\ y = w ) )
5 1 4 bitri 
 |-  ( <. z , w >. = <. x , y >. <-> ( x = z /\ y = w ) )
6 5 anbi1i 
 |-  ( ( <. z , w >. = <. x , y >. /\ ph ) <-> ( ( x = z /\ y = w ) /\ ph ) )
7 6 2exbii 
 |-  ( E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) <-> E. x E. y ( ( x = z /\ y = w ) /\ ph ) )
8 elopab 
 |-  ( <. z , w >. e. { <. x , y >. | ph } <-> E. x E. y ( <. z , w >. = <. x , y >. /\ ph ) )
9 2sb5 
 |-  ( [ z / x ] [ w / y ] ph <-> E. x E. y ( ( x = z /\ y = w ) /\ ph ) )
10 7 8 9 3bitr4i 
 |-  ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )