Description: Membership in a restriction. (Contributed by Scott Fenton, 17-Mar-2011) (Proof shortened by Peter Mazsa, 9-Sep-2022) Use the x B y idiom. (Revised by BJ, 16-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-elres | ⊢ ( 𝐴 ∈ ( 𝐵 ↾ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-res | ⊢ ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) ) | |
| 2 | 1 | eleq2i | ⊢ ( 𝐴 ∈ ( 𝐵 ↾ 𝐶 ) ↔ 𝐴 ∈ ( 𝐵 ∩ ( 𝐶 × V ) ) ) |
| 3 | bj-elinxp | ⊢ ( 𝐴 ∈ ( 𝐵 ∩ ( 𝐶 × V ) ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ V ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ) | |
| 4 | rexv | ⊢ ( ∃ 𝑦 ∈ V ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ↔ ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ) | |
| 5 | 4 | rexbii | ⊢ ( ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ∈ V ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ) |
| 6 | 2 3 5 | 3bitri | ⊢ ( 𝐴 ∈ ( 𝐵 ↾ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 𝐵 𝑦 ) ) |