Metamath Proof Explorer

Theorem rnmptpr

Description: Range of a function defined on an unordered pair. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses rnmptpr.a ⊢ φ → A ∈ V
rnmptpr.b ⊢ φ → B ∈ W
rnmptpr.f ⊢ F = x ∈ A B ⟼ C
rnmptpr.d ⊢ x = A → C = D
rnmptpr.e ⊢ x = B → C = E
Assertion rnmptpr ⊢ φ → ran ⁡ F = D E

Proof

Step Hyp Ref Expression
1 rnmptpr.a ⊢ φ → A ∈ V
2 rnmptpr.b ⊢ φ → B ∈ W
3 rnmptpr.f ⊢ F = x ∈ A B ⟼ C
4 rnmptpr.d ⊢ x = A → C = D
5 rnmptpr.e ⊢ x = B → C = E
6 4 eqeq2d ⊢ x = A → y = C ↔ y = D
7 5 eqeq2d ⊢ x = B → y = C ↔ y = E
8 6 7 rexprg ⊢ A ∈ V ∧ B ∈ W → ∃ x ∈ A B y = C ↔ y = D ∨ y = E
9 1 2 8 syl2anc ⊢ φ → ∃ x ∈ A B y = C ↔ y = D ∨ y = E
10 3 elrnmpt ⊢ y ∈ V → y ∈ ran ⁡ F ↔ ∃ x ∈ A B y = C
11 10 elv ⊢ y ∈ ran ⁡ F ↔ ∃ x ∈ A B y = C
12 vex ⊢ y ∈ V
13 12 elpr ⊢ y ∈ D E ↔ y = D ∨ y = E
14 9 11 13 3bitr4g ⊢ φ → y ∈ ran ⁡ F ↔ y ∈ D E
15 14 eqrdv ⊢ φ → ran ⁡ F = D E