Description: One direction of rabid2 is based on fewer axioms. (Contributed by Wolf Lammen, 26-May-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | rabid2im | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.71 | ⊢ ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) | |
2 | 1 | albii | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) ) |
3 | eqab | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) → 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ) | |
4 | 2 3 | sylbi | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ) |
5 | df-ral | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) | |
6 | df-rab | ⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } | |
7 | 6 | eqeq2i | ⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝜑 } ↔ 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ) |
8 | 4 5 7 | 3imtr4i | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝜑 } ) |