Metamath Proof Explorer


Theorem elorvc

Description: Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Hypotheses orvcval.1 φ Fun X
orvcval.2 φ X V
orvcval.3 φ A W
Assertion elorvc φ z dom X z X R RV/c A X z R A

Proof

Step Hyp Ref Expression
1 orvcval.1 φ Fun X
2 orvcval.2 φ X V
3 orvcval.3 φ A W
4 1 2 3 orvcval2 φ X R RV/c A = z dom X | X z R A
5 4 eleq2d φ z X R RV/c A z z dom X | X z R A
6 rabid z z dom X | X z R A z dom X X z R A
7 5 6 bitrdi φ z X R RV/c A z dom X X z R A
8 7 baibd φ z dom X z X R RV/c A X z R A