Description: Membership in a class abstraction of ordered pairs. Weaker version of elopab with a sethood antecedent, avoiding ax-sep , ax-nul , and ax-pr . Originally a subproof of elopab . (Contributed by SN, 11-Dec-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elopabw | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqeq1 | ⊢ ( 𝑧 = 𝐴 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ) | |
| 2 | 1 | anbi1d | ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) |
| 3 | 2 | 2exbidv | ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) |
| 4 | df-opab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } | |
| 5 | 3 4 | elab2g | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) |