Description: Equivalence of ordered pair abstraction equality and biconditional. Version of eqopab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Jan-2017) (Revised by Gino Giotto, 26-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | eqopab2bw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssopab2bw | ||
2 | ssopab2bw | ||
3 | 1 2 | anbi12i | |
4 | eqss | ||
5 | 2albiim | ||
6 | 3 4 5 | 3bitr4i |