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	⊢ Ⅎ 𝑦 𝐴
	cbvralcsf.2	⊢ Ⅎ 𝑥 𝐵
	cbvralcsf.3	⊢ Ⅎ 𝑦 𝜑
	cbvralcsf.4	⊢ Ⅎ 𝑥 𝜓
	cbvralcsf.5	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
	cbvralcsf.6	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvreucsf	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	⊢ Ⅎ 𝑦 𝐴
2		cbvralcsf.2	⊢ Ⅎ 𝑥 𝐵
3		cbvralcsf.3	⊢ Ⅎ 𝑦 𝜑
4		cbvralcsf.4	⊢ Ⅎ 𝑥 𝜓
5		cbvralcsf.5	⊢ ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
6		cbvralcsf.6	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
7		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝜑 )
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
9	8	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
10		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
11	9 10	nfan	⊢ Ⅎ 𝑥 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
12		id	⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
13		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
14	12 13	eleq12d	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
15		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
16	14 15	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
17	7 11 16	cbveu	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
18		nfcv	⊢ Ⅎ 𝑦 𝑧
19	18 1	nfcsb	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
20	19	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
21	3	nfsb	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
22	20 21	nfan	⊢ Ⅎ 𝑦 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 )
23		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐵 ∧ 𝜓 )
24		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
25		csbeq1	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
26		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 )
27	26	abbii	⊢ { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 } = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
28	2	nfcri	⊢ Ⅎ 𝑥 𝑣 ∈ 𝐵
29	5	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐵 ) )
30	28 29	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐵 )
31	30	bicomi	⊢ ( 𝑣 ∈ 𝐵 ↔ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 )
32	31	abbi2i	⊢ 𝐵 = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
33		df-csb	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
34	27 32 33	3eqtr4ri	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐵
35	25 34	eqtrdi	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐵 )
36	24 35	eleq12d	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
37		sbequ	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
38	4 6	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
39	37 38	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
40	36 39	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ) )
41	22 23 40	cbveu	⊢ ( ∃! 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) )
42	17 41	bitri	⊢ ( ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) )
43		df-reu	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
44		df-reu	⊢ ( ∃! 𝑦 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) )
45	42 43 44	3bitr4i	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 𝜓 )