Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999) Remove dependency on ax-13 . (Revised by Steven Nguyen, 23-Nov-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | elrab.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | elrab | ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elrab.1 | ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | elex | ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } → 𝐴 ∈ V ) | |
| 3 | elex | ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V ) | |
| 4 | 3 | adantr | ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) → 𝐴 ∈ V ) |
| 5 | eleq1 | ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) ) | |
| 6 | 5 1 | anbi12d | ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) ) |
| 7 | df-rab | ⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } | |
| 8 | 6 7 | elab2g | ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) ) |
| 9 | 2 4 8 | pm5.21nii | ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝐴 ∈ 𝐵 ∧ 𝜓 ) ) |