Metamath Proof Explorer


Theorem exopxfr2

Description: Transfer ordered-pair existence from/to single variable existence. (Contributed by NM, 26-Feb-2014)

Ref Expression
Hypothesis exopxfr2.1 x = y z φ ψ
Assertion exopxfr2 Rel A x A φ y z y z A ψ

Proof

Step Hyp Ref Expression
1 exopxfr2.1 x = y z φ ψ
2 df-rel Rel A A V × V
3 2 biimpi Rel A A V × V
4 3 sseld Rel A x A x V × V
5 4 adantrd Rel A x A φ x V × V
6 5 pm4.71rd Rel A x A φ x V × V x A φ
7 6 rexbidv2 Rel A x A φ x V × V x A φ
8 eleq1 x = y z x A y z A
9 8 1 anbi12d x = y z x A φ y z A ψ
10 9 exopxfr x V × V x A φ y z y z A ψ
11 7 10 bitrdi Rel A x A φ y z y z A ψ