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

Metamath Proof Explorer

Theorem ralxfrALT

Description: Alternate proof of ralxfr which does not use ralxfrd . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ralxfr.1 ⊢ y ∈ C → A ∈ B
ralxfr.2 ⊢ x ∈ B → ∃ y ∈ C x = A
ralxfr.3 ⊢ x = A → φ ↔ ψ
Assertion ralxfrALT ⊢ ∀ x ∈ B φ ↔ ∀ y ∈ C ψ

Proof

Step Hyp Ref Expression
1 ralxfr.1 ⊢ y ∈ C → A ∈ B
2 ralxfr.2 ⊢ x ∈ B → ∃ y ∈ C x = A
3 ralxfr.3 ⊢ x = A → φ ↔ ψ
4 3 rspcv ⊢ A ∈ B → ∀ x ∈ B φ → ψ
5 1 4 syl ⊢ y ∈ C → ∀ x ∈ B φ → ψ
6 5 com12 ⊢ ∀ x ∈ B φ → y ∈ C → ψ
7 6 ralrimiv ⊢ ∀ x ∈ B φ → ∀ y ∈ C ψ
8 nfra1 ⊢ Ⅎ y ∀ y ∈ C ψ
9 nfv ⊢ Ⅎ y φ
10 rsp ⊢ ∀ y ∈ C ψ → y ∈ C → ψ
11 3 biimprcd ⊢ ψ → x = A → φ
12 10 11 syl6 ⊢ ∀ y ∈ C ψ → y ∈ C → x = A → φ
13 8 9 12 rexlimd ⊢ ∀ y ∈ C ψ → ∃ y ∈ C x = A → φ
14 2 13 syl5 ⊢ ∀ y ∈ C ψ → x ∈ B → φ
15 14 ralrimiv ⊢ ∀ y ∈ C ψ → ∀ x ∈ B φ
16 7 15 impbii ⊢ ∀ x ∈ B φ ↔ ∀ y ∈ C ψ