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

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 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
rmoxfrd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
rmoxfrd.3 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion rmoxfrd ( 𝜑 → ( ∃* 𝑥 ∈ 𝐵 𝜓 ↔ ∃* 𝑦 ∈ 𝐶 𝜒 ) )

Proof

Step Hyp Ref Expression
1 rmoxfrd.1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
2 rmoxfrd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
3 rmoxfrd.3 ⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
4 reurex ⊢ ( ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
5 2 4 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
6 1 5 3 rexxfrd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑦 ∈ 𝐶 𝜒 ) )
7 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
8 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐶 𝜒 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) )
9 6 7 8 3bitr3g ⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) ) )
10 1 2 3 reuxfr1d ⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )
11 df-reu ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
12 df-reu ⊢ ( ∃! 𝑦 ∈ 𝐶 𝜒 ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) )
13 10 11 12 3bitr3g ⊢ ( 𝜑 → ( ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) ) )
14 9 13 imbi12d ⊢ ( 𝜑 → ( ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) → ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) ) ) )
15 moeu ⊢ ( ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) → ∃! 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) )
16 moeu ⊢ ( ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) ↔ ( ∃ 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) → ∃! 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) ) )
17 14 15 16 3bitr4g ⊢ ( 𝜑 → ( ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) ) )
18 df-rmo ⊢ ( ∃* 𝑥 ∈ 𝐵 𝜓 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
19 df-rmo ⊢ ( ∃* 𝑦 ∈ 𝐶 𝜒 ↔ ∃* 𝑦 ( 𝑦 ∈ 𝐶 ∧ 𝜒 ) )
20 17 18 19 3bitr4g ⊢ ( 𝜑 → ( ∃* 𝑥 ∈ 𝐵 𝜓 ↔ ∃* 𝑦 ∈ 𝐶 𝜒 ) )