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 bitrdi ∃! 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