Theorem bnj1468

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1468.1	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
	bnj1468.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	bnj1468.3	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
Assertion	bnj1468	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1468.1	⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
2		bnj1468.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		bnj1468.3	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
4		sbccow	⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 )
5		ax-5	⊢ ( 𝜓 → ∀ 𝑦 𝜓 )
6	3	nfcii	⊢ Ⅎ 𝑥 𝐴
7	6	nfeq2	⊢ Ⅎ 𝑥 𝑦 = 𝐴
8		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
9	1	nf5i	⊢ Ⅎ 𝑥 𝜓
10	8 9	nfbi	⊢ Ⅎ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
11	7 10	nfim	⊢ Ⅎ 𝑥 ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
12	11	nf5ri	⊢ ( ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ) → ∀ 𝑥 ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ) )
13		ax6ev	⊢ ∃ 𝑥 𝑥 = 𝑦
14		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
15	14 2	biimtrrdi	⊢ ( 𝑥 = 𝑦 → ( 𝑦 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) )
16		sbceq1a	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
17	16	bibi1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ↔ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ) )
18	15 17	sylibd	⊢ ( 𝑥 = 𝑦 → ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) ) )
19	13 18	bnj101	⊢ ∃ 𝑥 ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
20	12 19	bnj1131	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
21	5 20	bnj1464	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
22	4 21	bitr3id	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 ) )