Description: Sufficient condition for a collection of ordered pairs to be a subclass of a relation. (Contributed by Peter Mazsa, 21-Oct-2019) (Revised by Thierry Arnoux, 18-Feb-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | opabssi.1 | ⊢ ( 𝜑 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) | |
| Assertion | opabssi | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opabssi.1 | ⊢ ( 𝜑 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) | |
| 2 | df-opab | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } | |
| 3 | eleq1 | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) ) | |
| 4 | 3 | biimprd | ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → 𝑧 ∈ 𝐴 ) ) |
| 5 | 4 1 | impel | ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 ∈ 𝐴 ) |
| 6 | 5 | exlimivv | ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝑧 ∈ 𝐴 ) |
| 7 | 6 | abssi | ⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ⊆ 𝐴 |
| 8 | 2 7 | eqsstri | ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ 𝐴 |