This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmptpr

Description: Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017)

Ref Expression
Hypotheses fmptpr.1 ⊢ φ → A ∈ V
fmptpr.2 ⊢ φ → B ∈ W
fmptpr.3 ⊢ φ → C ∈ X
fmptpr.4 ⊢ φ → D ∈ Y
fmptpr.5 ⊢ φ ∧ x = A → E = C
fmptpr.6 ⊢ φ ∧ x = B → E = D
Assertion fmptpr ⊢ φ → A C B D = x ∈ A B ⟼ E

Proof

Step Hyp Ref Expression
1 fmptpr.1 ⊢ φ → A ∈ V
2 fmptpr.2 ⊢ φ → B ∈ W
3 fmptpr.3 ⊢ φ → C ∈ X
4 fmptpr.4 ⊢ φ → D ∈ Y
5 fmptpr.5 ⊢ φ ∧ x = A → E = C
6 fmptpr.6 ⊢ φ ∧ x = B → E = D
7 df-pr ⊢ A C B D = A C ∪ B D
8 7 a1i ⊢ φ → A C B D = A C ∪ B D
9 5 1 3 fmptsnd ⊢ φ → A C = x ∈ A ⟼ E
10 9 uneq1d ⊢ φ → A C ∪ B D = x ∈ A ⟼ E ∪ B D
11 df-pr ⊢ A B = A ∪ B
12 11 eqcomi ⊢ A ∪ B = A B
13 12 a1i ⊢ φ → A ∪ B = A B
14 2 4 13 6 fmptapd ⊢ φ → x ∈ A ⟼ E ∪ B D = x ∈ A B ⟼ E
15 8 10 14 3eqtrd ⊢ φ → A C B D = x ∈ A B ⟼ E