Metamath Proof Explorer

Theorem bnj1366

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1366.1 ⊢ ψ ↔ A ∈ V ∧ ∀ x ∈ A ∃! y φ ∧ B = y | ∃ x ∈ A φ
Assertion bnj1366 ⊢ ψ → B ∈ V

Proof

Step Hyp Ref Expression
1 bnj1366.1 ⊢ ψ ↔ A ∈ V ∧ ∀ x ∈ A ∃! y φ ∧ B = y | ∃ x ∈ A φ
2 1 simp3bi ⊢ ψ → B = y | ∃ x ∈ A φ
3 1 simp2bi ⊢ ψ → ∀ x ∈ A ∃! y φ
4 nfcv ⊢ Ⅎ _ y A
5 nfeu1 ⊢ Ⅎ y ∃! y φ
6 4 5 nfralw ⊢ Ⅎ y ∀ x ∈ A ∃! y φ
7 nfra1 ⊢ Ⅎ x ∀ x ∈ A ∃! y φ
8 rspa ⊢ ∀ x ∈ A ∃! y φ ∧ x ∈ A → ∃! y φ
9 iota1 ⊢ ∃! y φ → φ ↔ ι y | φ = y
10 eqcom ⊢ ι y | φ = y ↔ y = ι y | φ
11 9 10 syl6bb ⊢ ∃! y φ → φ ↔ y = ι y | φ
12 8 11 syl ⊢ ∀ x ∈ A ∃! y φ ∧ x ∈ A → φ ↔ y = ι y | φ
13 7 12 rexbida ⊢ ∀ x ∈ A ∃! y φ → ∃ x ∈ A φ ↔ ∃ x ∈ A y = ι y | φ
14 abid ⊢ y ∈ y | ∃ x ∈ A φ ↔ ∃ x ∈ A φ
15 eqid ⊢ x ∈ A ⟼ ι y | φ = x ∈ A ⟼ ι y | φ
16 iotaex ⊢ ι y | φ ∈ V
17 15 16 elrnmpti ⊢ y ∈ ran ⁡ x ∈ A ⟼ ι y | φ ↔ ∃ x ∈ A y = ι y | φ
18 13 14 17 3bitr4g ⊢ ∀ x ∈ A ∃! y φ → y ∈ y | ∃ x ∈ A φ ↔ y ∈ ran ⁡ x ∈ A ⟼ ι y | φ
19 6 18 alrimi ⊢ ∀ x ∈ A ∃! y φ → ∀ y y ∈ y | ∃ x ∈ A φ ↔ y ∈ ran ⁡ x ∈ A ⟼ ι y | φ
20 3 19 syl ⊢ ψ → ∀ y y ∈ y | ∃ x ∈ A φ ↔ y ∈ ran ⁡ x ∈ A ⟼ ι y | φ
21 nfab1 ⊢ Ⅎ _ y y | ∃ x ∈ A φ
22 nfiota1 ⊢ Ⅎ _ y ι y | φ
23 4 22 nfmpt ⊢ Ⅎ _ y x ∈ A ⟼ ι y | φ
24 23 nfrn ⊢ Ⅎ _ y ran ⁡ x ∈ A ⟼ ι y | φ
25 21 24 cleqf ⊢ y | ∃ x ∈ A φ = ran ⁡ x ∈ A ⟼ ι y | φ ↔ ∀ y y ∈ y | ∃ x ∈ A φ ↔ y ∈ ran ⁡ x ∈ A ⟼ ι y | φ
26 20 25 sylibr ⊢ ψ → y | ∃ x ∈ A φ = ran ⁡ x ∈ A ⟼ ι y | φ
27 2 26 eqtrd ⊢ ψ → B = ran ⁡ x ∈ A ⟼ ι y | φ
28 1 simp1bi ⊢ ψ → A ∈ V
29 mptexg ⊢ A ∈ V → x ∈ A ⟼ ι y | φ ∈ V
30 rnexg ⊢ x ∈ A ⟼ ι y | φ ∈ V → ran ⁡ x ∈ A ⟼ ι y | φ ∈ V
31 28 29 30 3syl ⊢ ψ → ran ⁡ x ∈ A ⟼ ι y | φ ∈ V
32 27 31 eqeltrd ⊢ ψ → B ∈ V