Theorem nfabd2

Description: Bound-variable hypothesis builder for a class abstraction. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Proof shortened by Wolf Lammen, 10-May-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfabd2.1	⊢ Ⅎ 𝑦 𝜑
	nfabd2.2	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
Assertion	nfabd2	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		nfabd2.1	⊢ Ⅎ 𝑦 𝜑
2		nfabd2.2	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
3		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
4	1 3	nfan	⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
5	4 2	nfabd	⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )
6	5	ex	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } ) )
7		nfab1	⊢ Ⅎ 𝑦 { 𝑦 ∣ 𝜓 }
8		eqidd	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { 𝑦 ∣ 𝜓 } = { 𝑦 ∣ 𝜓 } )
9	8	drnfc1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } ↔ Ⅎ 𝑦 { 𝑦 ∣ 𝜓 } ) )
10	7 9	mpbiri	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )
11	6 10	pm2.61d2	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ 𝜓 } )