elorvc

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

	Ref	Expression
Hypotheses	orvcval.1	$⊢ φ \to Fun X$
	orvcval.2	$⊢ φ \to X \in V$
	orvcval.3	$⊢ φ \to A \in W$
Assertion	elorvc	$⊢ (φ \land z \in dom X) \to (z \in (X R_{RV/c} A) \leftrightarrow X (z) R A)$

Step	Hyp	Ref	Expression
1		orvcval.1	$⊢ φ \to Fun X$
2		orvcval.2	$⊢ φ \to X \in V$
3		orvcval.3	$⊢ φ \to A \in W$
4	1 2 3	orvcval2	$⊢ φ \to X R_{RV/c} A = \{z \in dom X \| X (z) R A\}$
5	4	eleq2d	$⊢ φ \to (z \in (X R_{RV/c} A) \leftrightarrow z \in \{z \in dom X \| X (z) R A\})$
6		rabid	$⊢ z \in \{z \in dom X \| X (z) R A\} \leftrightarrow (z \in dom X \land X (z) R A)$
7	5 6	bitrdi	$⊢ φ \to (z \in (X R_{RV/c} A) \leftrightarrow (z \in dom X \land X (z) R A))$
8	7	baibd	$⊢ (φ \land z \in dom X) \to (z \in (X R_{RV/c} A) \leftrightarrow X (z) R A)$

Metamath Proof Explorer