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

Metamath Proof Explorer

Theorem brab

Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999)

Ref Expression
Hypotheses opelopab.1 ⊢ 𝐴 ∈ V
opelopab.2 ⊢ 𝐵 ∈ V
opelopab.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
opelopab.4 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
brab.5 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion brab ( 𝐴 𝑅 𝐵 ↔ 𝜒 )

Proof

Step Hyp Ref Expression
1 opelopab.1 ⊢ 𝐴 ∈ V
2 opelopab.2 ⊢ 𝐵 ∈ V
3 opelopab.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
4 opelopab.4 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
5 brab.5 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
6 3 4 5 brabg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 𝑅 𝐵 ↔ 𝜒 ) )
7 1 2 6 mp2an ⊢ ( 𝐴 𝑅 𝐵 ↔ 𝜒 )