Theorem rbropap

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 condition ps . (Contributed by AV, 31-Jan-2021)

	Ref	Expression
Hypotheses	rbropapd.1	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } )
	rbropapd.2	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	rbropap	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rbropapd.1	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ) } )
2		rbropapd.2	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
3	1 2	rbropapd	⊢ ( 𝜑 → ( ( 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) ) )
4	3	3impib	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) )