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 x y | φ z x w y φ

Proof

Step Hyp Ref Expression
1 eqcom z w = x y x y = z w
2 vex x V
3 vex y 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 φ x = z y = w φ
7 6 2exbii x y z w = x y φ x y x = z y = w φ
8 elopab z w x y | φ x y z w = x y φ
9 2sb5 z x w y φ x y x = z y = w φ
10 7 8 9 3bitr4i z w x y | φ z x w y φ