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

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) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 ralima.x ⊢ x = F ⁡ y → φ ↔ ψ
2 fnfun ⊢ F Fn A → Fun ⁡ F
3 2 funfnd ⊢ F Fn A → F Fn dom ⁡ F
4 fndm ⊢ F Fn A → dom ⁡ F = A
5 4 sseq2d ⊢ F Fn A → B ⊆ dom ⁡ F ↔ B ⊆ A
6 5 biimpar ⊢ F Fn A ∧ B ⊆ A → B ⊆ dom ⁡ F
7 fvexd ⊢ F Fn dom ⁡ F ∧ B ⊆ dom ⁡ F ∧ y ∈ B → F ⁡ y ∈ V
8 fvelimab ⊢ F Fn dom ⁡ F ∧ B ⊆ dom ⁡ F → x ∈ F B ↔ ∃ y ∈ B F ⁡ y = x
9 eqcom ⊢ F ⁡ y = x ↔ x = F ⁡ y
10 9 rexbii ⊢ ∃ y ∈ B F ⁡ y = x ↔ ∃ y ∈ B x = F ⁡ y
11 8 10 bitrdi ⊢ F Fn dom ⁡ F ∧ B ⊆ dom ⁡ F → x ∈ F B ↔ ∃ y ∈ B x = F ⁡ y
12 1 adantl ⊢ F Fn dom ⁡ F ∧ B ⊆ dom ⁡ F ∧ x = F ⁡ y → φ ↔ ψ
13 7 11 12 ralxfr2d ⊢ F Fn dom ⁡ F ∧ B ⊆ dom ⁡ F → ∀ x ∈ F B φ ↔ ∀ y ∈ B ψ
14 3 6 13 syl2an2r ⊢ F Fn A ∧ B ⊆ A → ∀ x ∈ F B φ ↔ ∀ y ∈ B ψ