Description: Obsolete version of elopaelxp as of 11-Dec-2024. (Contributed by Alexander van der Vekens, 23-Jun-2018) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elopaelxpOLD | ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → 𝐴 ∈ ( V × V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl | ⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) | |
| 2 | 1 | 2eximi | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) |
| 3 | elopab | ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) | |
| 4 | elvv | ⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) | |
| 5 | 2 3 4 | 3imtr4i | ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } → 𝐴 ∈ ( V × V ) ) |