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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom | ||
2 | vex | ||
3 | vex | ||
4 | 2 3 | opth | |
5 | 1 4 | bitri | |
6 | 5 | anbi1i | |
7 | 6 | 2exbii | |
8 | elopab | ||
9 | 2sb5 | ||
10 | 7 8 9 | 3bitr4i |