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

Metamath Proof Explorer

Theorem elopabi

Description: A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006)

Ref Expression
Hypotheses elopabi.1 ⊢ x = 1 st ⁡ A → φ ↔ ψ
elopabi.2 ⊢ y = 2 nd ⁡ A → ψ ↔ χ
Assertion elopabi ⊢ A ∈ x y | φ → χ

Proof

Step Hyp Ref Expression
1 elopabi.1 ⊢ x = 1 st ⁡ A → φ ↔ ψ
2 elopabi.2 ⊢ y = 2 nd ⁡ A → ψ ↔ χ
3 relopabv ⊢ Rel ⁡ x y | φ
4 1st2nd ⊢ Rel ⁡ x y | φ ∧ A ∈ x y | φ → A = 1 st ⁡ A 2 nd ⁡ A
5 3 4 mpan ⊢ A ∈ x y | φ → A = 1 st ⁡ A 2 nd ⁡ A
6 id ⊢ A ∈ x y | φ → A ∈ x y | φ
7 5 6 eqeltrrd ⊢ A ∈ x y | φ → 1 st ⁡ A 2 nd ⁡ A ∈ x y | φ
8 fvex ⊢ 1 st ⁡ A ∈ V
9 fvex ⊢ 2 nd ⁡ A ∈ V
10 8 9 1 2 opelopab ⊢ 1 st ⁡ A 2 nd ⁡ A ∈ x y | φ ↔ χ
11 7 10 sylib ⊢ A ∈ x y | φ → χ