Theorem ralab2

Description: Universal quantification over a class abstraction. (Contributed by Mario Carneiro, 3-Sep-2015) Drop ax-8 . (Revised by Gino Giotto, 1-Dec-2023)

	Ref	Expression
Hypothesis	ralab2.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
Assertion	ralab2	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∀ 𝑦 ( 𝜑 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		ralab2.1	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } → 𝜓 ) )
3		nfsab1	⊢ Ⅎ 𝑦 𝑥 ∈ { 𝑦 ∣ 𝜑 }
4		nfv	⊢ Ⅎ 𝑦 𝜓
5	3 4	nfim	⊢ Ⅎ 𝑦 ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } → 𝜓 )
6		nfv	⊢ Ⅎ 𝑥 ( 𝜑 → 𝜒 )
7		eleq1ab	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑦 ∣ 𝜑 } ) )
8		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 )
9	7 8	bitrdi	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝜑 ) )
10	9 1	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } → 𝜓 ) ↔ ( 𝜑 → 𝜒 ) ) )
11	5 6 10	cbvalv1	⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ 𝜑 } → 𝜓 ) ↔ ∀ 𝑦 ( 𝜑 → 𝜒 ) )
12	2 11	bitri	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ 𝜑 } 𝜓 ↔ ∀ 𝑦 ( 𝜑 → 𝜒 ) )