Metamath Proof Explorer

Theorem ralima

Description: Universal quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 rexima.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 syl6bb ⊢ 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 ψ