rbropapd

Description: Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017)

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

Step	Hyp	Ref	Expression
1		rbropapd.1	$⊢ φ \to M = \{⟨f, p⟩ \| (f W p \land ψ)\}$
2		rbropapd.2	$⊢ (f = F \land p = P) \to (ψ \leftrightarrow χ)$
3		df-br	$⊢ F M P \leftrightarrow ⟨F, P⟩ \in M$
4	1	eleq2d	$⊢ φ \to (⟨F, P⟩ \in M \leftrightarrow ⟨F, P⟩ \in \{⟨f, p⟩ \| (f W p \land ψ)\})$
5	3 4	syl5bb	$⊢ φ \to (F M P \leftrightarrow ⟨F, P⟩ \in \{⟨f, p⟩ \| (f W p \land ψ)\})$
6		breq12	$⊢ (f = F \land p = P) \to (f W p \leftrightarrow F W P)$
7	6 2	anbi12d	$⊢ (f = F \land p = P) \to ((f W p \land ψ) \leftrightarrow (F W P \land χ))$
8	7	opelopabga	$⊢ (F \in X \land P \in Y) \to (⟨F, P⟩ \in \{⟨f, p⟩ \| (f W p \land ψ)\} \leftrightarrow (F W P \land χ))$
9	5 8	sylan9bb	$⊢ (φ \land (F \in X \land P \in Y)) \to (F M P \leftrightarrow (F W P \land χ))$
10	9	ex	$⊢ φ \to ((F \in X \land P \in Y) \to (F M P \leftrightarrow (F W P \land χ)))$

Metamath Proof Explorer