Theorem gencbval

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996)

	Ref	Expression
Hypotheses	gencbval.1	⊢ 𝐴 ∈ V
	gencbval.2	⊢ ( 𝐴 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	gencbval.3	⊢ ( 𝐴 = 𝑦 → ( 𝜒 ↔ 𝜃 ) )
	gencbval.4	⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
Assertion	gencbval	⊢ ( ∀ 𝑥 ( 𝜒 → 𝜑 ) ↔ ∀ 𝑦 ( 𝜃 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		gencbval.1	⊢ 𝐴 ∈ V
2		gencbval.2	⊢ ( 𝐴 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		gencbval.3	⊢ ( 𝐴 = 𝑦 → ( 𝜒 ↔ 𝜃 ) )
4		gencbval.4	⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
5	2	notbid	⊢ ( 𝐴 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
6	1 5 3 4	gencbvex	⊢ ( ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜑 ) ↔ ∃ 𝑦 ( 𝜃 ∧ ¬ 𝜓 ) )
7		exanali	⊢ ( ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝜒 → 𝜑 ) )
8		exanali	⊢ ( ∃ 𝑦 ( 𝜃 ∧ ¬ 𝜓 ) ↔ ¬ ∀ 𝑦 ( 𝜃 → 𝜓 ) )
9	6 7 8	3bitr3i	⊢ ( ¬ ∀ 𝑥 ( 𝜒 → 𝜑 ) ↔ ¬ ∀ 𝑦 ( 𝜃 → 𝜓 ) )
10	9	con4bii	⊢ ( ∀ 𝑥 ( 𝜒 → 𝜑 ) ↔ ∀ 𝑦 ( 𝜃 → 𝜓 ) )