Metamath Proof Explorer

Theorem rmoxfrd

Description: Transfer "at most one" restricted quantification from a variable x to another variable y contained in expression A . (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmoxfrd.1 ⊢ φ ∧ y ∈ C → A ∈ B
rmoxfrd.2 ⊢ φ ∧ x ∈ B → ∃! y ∈ C x = A
rmoxfrd.3 ⊢ φ ∧ x = A → ψ ↔ χ
Assertion rmoxfrd ⊢ φ → ∃* x ∈ B ψ ↔ ∃* y ∈ C χ

Proof

Step Hyp Ref Expression
1 rmoxfrd.1 ⊢ φ ∧ y ∈ C → A ∈ B
2 rmoxfrd.2 ⊢ φ ∧ x ∈ B → ∃! y ∈ C x = A
3 rmoxfrd.3 ⊢ φ ∧ x = A → ψ ↔ χ
4 reurex ⊢ ∃! y ∈ C x = A → ∃ y ∈ C x = A
5 2 4 syl ⊢ φ ∧ x ∈ B → ∃ y ∈ C x = A
6 1 5 3 rexxfrd ⊢ φ → ∃ x ∈ B ψ ↔ ∃ y ∈ C χ
7 df-rex ⊢ ∃ x ∈ B ψ ↔ ∃ x x ∈ B ∧ ψ
8 df-rex ⊢ ∃ y ∈ C χ ↔ ∃ y y ∈ C ∧ χ
9 6 7 8 3bitr3g ⊢ φ → ∃ x x ∈ B ∧ ψ ↔ ∃ y y ∈ C ∧ χ
10 1 2 3 reuxfr1d ⊢ φ → ∃! x ∈ B ψ ↔ ∃! y ∈ C χ
11 df-reu ⊢ ∃! x ∈ B ψ ↔ ∃! x x ∈ B ∧ ψ
12 df-reu ⊢ ∃! y ∈ C χ ↔ ∃! y y ∈ C ∧ χ
13 10 11 12 3bitr3g ⊢ φ → ∃! x x ∈ B ∧ ψ ↔ ∃! y y ∈ C ∧ χ
14 9 13 imbi12d ⊢ φ → ∃ x x ∈ B ∧ ψ → ∃! x x ∈ B ∧ ψ ↔ ∃ y y ∈ C ∧ χ → ∃! y y ∈ C ∧ χ
15 moeu ⊢ ∃* x x ∈ B ∧ ψ ↔ ∃ x x ∈ B ∧ ψ → ∃! x x ∈ B ∧ ψ
16 moeu ⊢ ∃* y y ∈ C ∧ χ ↔ ∃ y y ∈ C ∧ χ → ∃! y y ∈ C ∧ χ
17 14 15 16 3bitr4g ⊢ φ → ∃* x x ∈ B ∧ ψ ↔ ∃* y y ∈ C ∧ χ
18 df-rmo ⊢ ∃* x ∈ B ψ ↔ ∃* x x ∈ B ∧ ψ
19 df-rmo ⊢ ∃* y ∈ C χ ↔ ∃* y y ∈ C ∧ χ
20 17 18 19 3bitr4g ⊢ φ → ∃* x ∈ B ψ ↔ ∃* y ∈ C χ