Metamath Proof Explorer

Theorem opelopabsbALT

Description: The law of concretion in terms of substitutions. Less general than opelopabsb , but having a much shorter proof. (Contributed by NM, 30-Sep-2002) (Proof shortened by Andrew Salmon, 25-Jul-2011) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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