Metamath Proof Explorer


Theorem brabd

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023)

Ref Expression
Hypotheses brabd.exa φAU
brabd.exb φBV
brabd.def φR=xy|ψ
brabd.is φx=Ay=Bψχ
Assertion brabd φARBχ

Proof

Step Hyp Ref Expression
1 brabd.exa φAU
2 brabd.exb φBV
3 brabd.def φR=xy|ψ
4 brabd.is φx=Ay=Bψχ
5 ax-5 φxφ
6 ax-5 φyφ
7 nfvd φxχ
8 nfvd φyχ
9 5 6 7 8 1 2 3 4 brabd0 φARBχ