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

Metamath Proof Explorer

Theorem brab2a

Description: The law of concretion for a binary relation. Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Hypotheses brab2a.1 ⊢ x = A ∧ y = B → φ ↔ ψ
brab2a.2 ⊢ R = x y | x ∈ C ∧ y ∈ D ∧ φ
Assertion brab2a ⊢ A R B ↔ A ∈ C ∧ B ∈ D ∧ ψ

Proof

Step Hyp Ref Expression
1 brab2a.1 ⊢ x = A ∧ y = B → φ ↔ ψ
2 brab2a.2 ⊢ R = x y | x ∈ C ∧ y ∈ D ∧ φ
3 opabssxp ⊢ x y | x ∈ C ∧ y ∈ D ∧ φ ⊆ C × D
4 2 3 eqsstri ⊢ R ⊆ C × D
5 4 brel ⊢ A R B → A ∈ C ∧ B ∈ D
6 df-br ⊢ A R B ↔ A B ∈ R
7 2 eleq2i ⊢ A B ∈ R ↔ A B ∈ x y | x ∈ C ∧ y ∈ D ∧ φ
8 6 7 bitri ⊢ A R B ↔ A B ∈ x y | x ∈ C ∧ y ∈ D ∧ φ
9 1 opelopab2a ⊢ A ∈ C ∧ B ∈ D → A B ∈ x y | x ∈ C ∧ y ∈ D ∧ φ ↔ ψ
10 8 9 bitrid ⊢ A ∈ C ∧ B ∈ D → A R B ↔ ψ
11 5 10 biadanii ⊢ A R B ↔ A ∈ C ∧ B ∈ D ∧ ψ