Metamath Proof Explorer

Theorem brabg2

Description: Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses brabg2.1 ⊢ x = A → φ ↔ ψ
brabg2.2 ⊢ y = B → ψ ↔ χ
brabg2.3 ⊢ R = x y | φ
brabg2.4 ⊢ χ → A ∈ C
Assertion brabg2 ⊢ B ∈ D → A R B ↔ χ

Proof

Step Hyp Ref Expression
1 brabg2.1 ⊢ x = A → φ ↔ ψ
2 brabg2.2 ⊢ y = B → ψ ↔ χ
3 brabg2.3 ⊢ R = x y | φ
4 brabg2.4 ⊢ χ → A ∈ C
5 3 relopabiv ⊢ Rel ⁡ R
6 5 brrelex1i ⊢ A R B → A ∈ V
7 1 2 3 brabg ⊢ A ∈ V ∧ B ∈ D → A R B ↔ χ
8 7 biimpd ⊢ A ∈ V ∧ B ∈ D → A R B → χ
9 8 ex ⊢ A ∈ V → B ∈ D → A R B → χ
10 9 com3l ⊢ B ∈ D → A R B → A ∈ V → χ
11 6 10 mpdi ⊢ B ∈ D → A R B → χ
12 1 2 3 brabg ⊢ A ∈ C ∧ B ∈ D → A R B ↔ χ
13 12 exbiri ⊢ A ∈ C → B ∈ D → χ → A R B
14 13 com3l ⊢ B ∈ D → χ → A ∈ C → A R B
15 4 14 mpdi ⊢ B ∈ D → χ → A R B
16 11 15 impbid ⊢ B ∈ D → A R B ↔ χ