Metamath Proof Explorer

Theorem 2rbropap

Description: Properties of a pair in a restricted binary relation M expressed as an ordered-pair class abstraction: M is the binary relation W restricted by the conditions ps and ta . (Contributed by AV, 31-Jan-2021)

		Ref	Expression
	Hypotheses	2rbropap.1	$⊢ φ \to M = \{⟨f, p⟩ \| (f W p \land ψ \land τ)\}$
		2rbropap.2	$⊢ (f = F \land p = P) \to (ψ \leftrightarrow χ)$
		2rbropap.3	$⊢ (f = F \land p = P) \to (τ \leftrightarrow θ)$
	Assertion	2rbropap	$⊢ (φ \land F \in X \land P \in Y) \to (F M P \leftrightarrow (F W P \land χ \land θ))$

Proof

Step	Hyp	Ref	Expression
1		2rbropap.1	$⊢ φ \to M = \{⟨f, p⟩ \| (f W p \land ψ \land τ)\}$
2		2rbropap.2	$⊢ (f = F \land p = P) \to (ψ \leftrightarrow χ)$
3		2rbropap.3	$⊢ (f = F \land p = P) \to (τ \leftrightarrow θ)$
4		3anass	$⊢ (f W p \land ψ \land τ) \leftrightarrow (f W p \land (ψ \land τ))$
5	4	opabbii	$⊢ \{⟨f, p⟩ \| (f W p \land ψ \land τ)\} = \{⟨f, p⟩ \| (f W p \land (ψ \land τ))\}$
6	1 5	eqtrdi	$⊢ φ \to M = \{⟨f, p⟩ \| (f W p \land (ψ \land τ))\}$
7	2 3	anbi12d	$⊢ (f = F \land p = P) \to ((ψ \land τ) \leftrightarrow (χ \land θ))$
8	6 7	rbropap	$⊢ (φ \land F \in X \land P \in Y) \to (F M P \leftrightarrow (F W P \land (χ \land θ)))$
9		3anass	$⊢ (F W P \land χ \land θ) \leftrightarrow (F W P \land (χ \land θ))$
10	8 9	bitr4di	$⊢ (φ \land F \in X \land P \in Y) \to (F M P \leftrightarrow (F W P \land χ \land θ))$