Theorem 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	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } )
	rbropapd.2	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	rbropapd	⊢ ( 𝜑 → ( ( 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		rbropapd.1	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } )
2		rbropapd.2	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
3		df-br	⊢ ( 𝐹 𝑀 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ 𝑀 )
4	1	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ 𝑀 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } ) )
5	3 4	bitrid	⊢ ( 𝜑 → ( 𝐹 𝑀 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } ) )
6		breq12	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑓 𝑊 𝑝 ↔ 𝐹 𝑊 𝑃 ) )
7	6 2	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) )
8	7	opelopabga	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( ⟨ 𝐹 , 𝑃 ⟩ ∈ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) )
9	5 8	sylan9bb	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) )
10	9	ex	⊢ ( 𝜑 → ( ( 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) ) )