Metamath Proof Explorer


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 ( ∀ 𝑥 ∈ { 𝑦𝜑 } 𝜓 ↔ ∀ 𝑦 ( 𝜑𝜒 ) )