Metamath Proof Explorer

Theorem elsnres

Description: Membership in restriction to a singleton. (Contributed by Scott Fenton, 17-Mar-2011)

Ref Expression
Hypothesis elsnres.1 ⊢ C ∈ V
Assertion elsnres ⊢ A ∈ B ↾ C ↔ ∃ y A = C y ∧ C y ∈ B

Proof

Step Hyp Ref Expression
1 elsnres.1 ⊢ C ∈ V
2 elres ⊢ A ∈ B ↾ C ↔ ∃ x ∈ C ∃ y A = x y ∧ x y ∈ B
3 rexcom4 ⊢ ∃ x ∈ C ∃ y A = x y ∧ x y ∈ B ↔ ∃ y ∃ x ∈ C A = x y ∧ x y ∈ B
4 opeq1 ⊢ x = C → x y = C y
5 4 eqeq2d ⊢ x = C → A = x y ↔ A = C y
6 4 eleq1d ⊢ x = C → x y ∈ B ↔ C y ∈ B
7 5 6 anbi12d ⊢ x = C → A = x y ∧ x y ∈ B ↔ A = C y ∧ C y ∈ B
8 1 7 rexsn ⊢ ∃ x ∈ C A = x y ∧ x y ∈ B ↔ A = C y ∧ C y ∈ B
9 8 exbii ⊢ ∃ y ∃ x ∈ C A = x y ∧ x y ∈ B ↔ ∃ y A = C y ∧ C y ∈ B
10 2 3 9 3bitri ⊢ A ∈ B ↾ C ↔ ∃ y A = C y ∧ C y ∈ B