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

Proof

Step	Hyp	Ref	Expression
1		2rbropap.1	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) } )
2		2rbropap.2	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜓 ↔ 𝜒 ) )
3		2rbropap.3	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝜏 ↔ 𝜃 ) )
4		3anass	⊢ ( ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) ↔ ( 𝑓 𝑊 𝑝 ∧ ( 𝜓 ∧ 𝜏 ) ) )
5	4	opabbii	⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ 𝜓 ∧ 𝜏 ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ ( 𝜓 ∧ 𝜏 ) ) }
6	1 5	eqtrdi	⊢ ( 𝜑 → 𝑀 = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 𝑊 𝑝 ∧ ( 𝜓 ∧ 𝜏 ) ) } )
7	2 3	anbi12d	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝜓 ∧ 𝜏 ) ↔ ( 𝜒 ∧ 𝜃 ) ) )
8	6 7	rbropap	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ ( 𝜒 ∧ 𝜃 ) ) ) )
9		3anass	⊢ ( ( 𝐹 𝑊 𝑃 ∧ 𝜒 ∧ 𝜃 ) ↔ ( 𝐹 𝑊 𝑃 ∧ ( 𝜒 ∧ 𝜃 ) ) )
10	8 9	bitr4di	⊢ ( ( 𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ∧ 𝜃 ) ) )