Description: Alternate proof of abv , shorter but using more axioms. (Contributed by BJ, 19-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | abvALT | ⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab | ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 ) | |
2 | 1 | albii | ⊢ ( ∀ 𝑦 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) |
3 | eqv | ⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑦 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) | |
4 | nfv | ⊢ Ⅎ 𝑦 𝜑 | |
5 | 4 | sb8v | ⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) |
6 | 2 3 5 | 3bitr4i | ⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 ) |