This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌 ) → ( 𝐹 𝑀 𝑃 ↔ ( 𝐹 𝑊 𝑃 ∧ 𝜒 ) ) ) )