Metamath Proof Explorer

Theorem mptssid

Description: The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses mptssid.1 ⊢ Ⅎ _ x A
mptssid.2 ⊢ C = x ∈ A | B ∈ V
Assertion mptssid ⊢ x ∈ A ⟼ B = x ∈ C ⟼ B

Proof

Step Hyp Ref Expression
1 mptssid.1 ⊢ Ⅎ _ x A
2 mptssid.2 ⊢ C = x ∈ A | B ∈ V
3 eqvisset ⊢ y = B → B ∈ V
4 3 anim2i ⊢ x ∈ A ∧ y = B → x ∈ A ∧ B ∈ V
5 rabid ⊢ x ∈ x ∈ A | B ∈ V ↔ x ∈ A ∧ B ∈ V
6 4 5 sylibr ⊢ x ∈ A ∧ y = B → x ∈ x ∈ A | B ∈ V
7 6 2 eleqtrrdi ⊢ x ∈ A ∧ y = B → x ∈ C
8 simpr ⊢ x ∈ A ∧ y = B → y = B
9 7 8 jca ⊢ x ∈ A ∧ y = B → x ∈ C ∧ y = B
10 1 ssrab2f ⊢ x ∈ A | B ∈ V ⊆ A
11 2 10 eqsstri ⊢ C ⊆ A
12 11 sseli ⊢ x ∈ C → x ∈ A
13 12 anim1i ⊢ x ∈ C ∧ y = B → x ∈ A ∧ y = B
14 9 13 impbii ⊢ x ∈ A ∧ y = B ↔ x ∈ C ∧ y = B
15 14 opabbii ⊢ x y | x ∈ A ∧ y = B = x y | x ∈ C ∧ y = B
16 df-mpt ⊢ x ∈ A ⟼ B = x y | x ∈ A ∧ y = B
17 df-mpt ⊢ x ∈ C ⟼ B = x y | x ∈ C ∧ y = B
18 15 16 17 3eqtr4i ⊢ x ∈ A ⟼ B = x ∈ C ⟼ B