Metamath Proof Explorer


Theorem ssoprab2b

Description: Equivalence of ordered pair abstraction subclass and implication. Compare ssopab2b . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by FL, 6-Nov-2013) (Proof shortened by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)

Ref Expression
Assertion ssoprab2b xyz|φxyz|ψxyzφψ

Proof

Step Hyp Ref Expression
1 nfoprab1 _xxyz|φ
2 nfoprab1 _xxyz|ψ
3 1 2 nfss xxyz|φxyz|ψ
4 nfoprab2 _yxyz|φ
5 nfoprab2 _yxyz|ψ
6 4 5 nfss yxyz|φxyz|ψ
7 nfoprab3 _zxyz|φ
8 nfoprab3 _zxyz|ψ
9 7 8 nfss zxyz|φxyz|ψ
10 ssel xyz|φxyz|ψxyzxyz|φxyzxyz|ψ
11 oprabid xyzxyz|φφ
12 oprabid xyzxyz|ψψ
13 10 11 12 3imtr3g xyz|φxyz|ψφψ
14 9 13 alrimi xyz|φxyz|ψzφψ
15 6 14 alrimi xyz|φxyz|ψyzφψ
16 3 15 alrimi xyz|φxyz|ψxyzφψ
17 ssoprab2 xyzφψxyz|φxyz|ψ
18 16 17 impbii xyz|φxyz|ψxyzφψ