cbvralcsf

Description: A more general version of cbvralf that doesn't require A and B to be distinct from x or y . 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	cbvralcsf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 )

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		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
11	9 10	nfim	⊢ Ⅎ 𝑥 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 )
12		id	⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
13		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
14	12 13	eleq12d	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
15		sbceq1a	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
16	14 15	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
17	7 11 16	cbvalv1	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) )
18		nfcv	⊢ Ⅎ 𝑦 𝑧
19	18 1	nfcsb	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐴
20	19	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴
21	18 3	nfsbc	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
22	20 21	nfim	⊢ Ⅎ 𝑦 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 )
23		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐵 → 𝜓 )
24		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
25		csbeq1	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
26		df-csb	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
27	2	nfcri	⊢ Ⅎ 𝑥 𝑣 ∈ 𝐵
28	5	eleq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐵 ) )
29	27 28	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐵 )
30		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 )
31	29 30	bitr3i	⊢ ( 𝑣 ∈ 𝐵 ↔ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 )
32	31	eqabi	⊢ 𝐵 = { 𝑣 ∣ [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 }
33	26 32	eqtr4i	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐵
34	25 33	eqtrdi	⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐵 )
35	24 34	eleq12d	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
36		dfsbcq	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
37		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
38	4 6	sbie	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
39	37 38	bitr3i	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
40	36 39	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
41	35 40	imbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐵 → 𝜓 ) ) )
42	22 23 41	cbvalv1	⊢ ( ∀ 𝑧 ( 𝑧 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜓 ) )
43	17 42	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜓 ) )
44		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
45		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐵 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝜓 ) )
46	43 44 45	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 𝜓 )

Metamath Proof Explorer

Theorem cbvralcsf

Proof