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

Metamath Proof Explorer

Theorem ralimaOLD

Description: Obsolete version of ralima as of 14-Aug-2025. (Contributed by Stefan O'Rear, 21-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis reximaOLD.x ⊢ x = F ⁡ y → φ ↔ ψ
Assertion ralimaOLD ⊢ F Fn A ∧ B ⊆ A → ∀ x ∈ F B φ ↔ ∀ y ∈ B ψ

Proof

Step Hyp Ref Expression
1 reximaOLD.x ⊢ x = F ⁡ y → φ ↔ ψ
2 fvexd ⊢ F Fn A ∧ B ⊆ A ∧ y ∈ B → F ⁡ y ∈ V
3 fvelimab ⊢ F Fn A ∧ B ⊆ A → x ∈ F B ↔ ∃ y ∈ B F ⁡ y = x
4 eqcom ⊢ F ⁡ y = x ↔ x = F ⁡ y
5 4 rexbii ⊢ ∃ y ∈ B F ⁡ y = x ↔ ∃ y ∈ B x = F ⁡ y
6 3 5 bitrdi ⊢ F Fn A ∧ B ⊆ A → x ∈ F B ↔ ∃ y ∈ B x = F ⁡ y
7 1 adantl ⊢ F Fn A ∧ B ⊆ A ∧ x = F ⁡ y → φ ↔ ψ
8 2 6 7 ralxfr2d ⊢ F Fn A ∧ B ⊆ A → ∀ x ∈ F B φ ↔ ∀ y ∈ B ψ