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

Metamath Proof Explorer

Theorem cbvreucsf

Description: A more general version of cbvreuv that has no distinct variable restrictions. Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cbvralcsf.1 ⊢ Ⅎ _ y A
cbvralcsf.2 ⊢ Ⅎ _ x B
cbvralcsf.3 ⊢ Ⅎ y φ
cbvralcsf.4 ⊢ Ⅎ x ψ
cbvralcsf.5 ⊢ x = y → A = B
cbvralcsf.6 ⊢ x = y → φ ↔ ψ
Assertion cbvreucsf ⊢ ∃! x ∈ A φ ↔ ∃! y ∈ B ψ

Proof

Step Hyp Ref Expression
1 cbvralcsf.1 ⊢ Ⅎ _ y A
2 cbvralcsf.2 ⊢ Ⅎ _ x B
3 cbvralcsf.3 ⊢ Ⅎ y φ
4 cbvralcsf.4 ⊢ Ⅎ x ψ
5 cbvralcsf.5 ⊢ x = y → A = B
6 cbvralcsf.6 ⊢ x = y → φ ↔ ψ
7 nfv ⊢ Ⅎ z x ∈ A ∧ φ
8 nfcsb1v ⊢ Ⅎ _ x ⦋ z / x⦌ A
9 8 nfcri ⊢ Ⅎ x z ∈ ⦋ z / x⦌ A
10 nfs1v ⊢ Ⅎ x z x φ
11 9 10 nfan ⊢ Ⅎ x z ∈ ⦋ z / x⦌ A ∧ z x φ
12 id ⊢ x = z → x = z
13 csbeq1a ⊢ x = z → A = ⦋ z / x⦌ A
14 12 13 eleq12d ⊢ x = z → x ∈ A ↔ z ∈ ⦋ z / x⦌ A
15 sbequ12 ⊢ x = z → φ ↔ z x φ
16 14 15 anbi12d ⊢ x = z → x ∈ A ∧ φ ↔ z ∈ ⦋ z / x⦌ A ∧ z x φ
17 7 11 16 cbveu ⊢ ∃! x x ∈ A ∧ φ ↔ ∃! z z ∈ ⦋ z / x⦌ A ∧ z x φ
18 nfcv ⊢ Ⅎ _ y z
19 18 1 nfcsb ⊢ Ⅎ _ y ⦋ z / x⦌ A
20 19 nfcri ⊢ Ⅎ y z ∈ ⦋ z / x⦌ A
21 3 nfsb ⊢ Ⅎ y z x φ
22 20 21 nfan ⊢ Ⅎ y z ∈ ⦋ z / x⦌ A ∧ z x φ
23 nfv ⊢ Ⅎ z y ∈ B ∧ ψ
24 id ⊢ z = y → z = y
25 csbeq1 ⊢ z = y → ⦋ z / x⦌ A = ⦋ y / x⦌ A
26 sbsbc ⊢ y x v ∈ A ↔ [˙y / x]˙ v ∈ A
27 26 abbii ⊢ v | y x v ∈ A = v | [˙y / x]˙ v ∈ A
28 2 nfcri ⊢ Ⅎ x v ∈ B
29 5 eleq2d ⊢ x = y → v ∈ A ↔ v ∈ B
30 28 29 sbie ⊢ y x v ∈ A ↔ v ∈ B
31 30 bicomi ⊢ v ∈ B ↔ y x v ∈ A
32 31 eqabi ⊢ B = v | y x v ∈ A
33 df-csb ⊢ ⦋ y / x⦌ A = v | [˙y / x]˙ v ∈ A
34 27 32 33 3eqtr4ri ⊢ ⦋ y / x⦌ A = B
35 25 34 eqtrdi ⊢ z = y → ⦋ z / x⦌ A = B
36 24 35 eleq12d ⊢ z = y → z ∈ ⦋ z / x⦌ A ↔ y ∈ B
37 sbequ ⊢ z = y → z x φ ↔ y x φ
38 4 6 sbie ⊢ y x φ ↔ ψ
39 37 38 bitrdi ⊢ z = y → z x φ ↔ ψ
40 36 39 anbi12d ⊢ z = y → z ∈ ⦋ z / x⦌ A ∧ z x φ ↔ y ∈ B ∧ ψ
41 22 23 40 cbveu ⊢ ∃! z z ∈ ⦋ z / x⦌ A ∧ z x φ ↔ ∃! y y ∈ B ∧ ψ
42 17 41 bitri ⊢ ∃! x x ∈ A ∧ φ ↔ ∃! y y ∈ B ∧ ψ
43 df-reu ⊢ ∃! x ∈ A φ ↔ ∃! x x ∈ A ∧ φ
44 df-reu ⊢ ∃! y ∈ B ψ ↔ ∃! y y ∈ B ∧ ψ
45 42 43 44 3bitr4i ⊢ ∃! x ∈ A φ ↔ ∃! y ∈ B ψ