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 )