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

Metamath Proof Explorer

Theorem reusv2

Description: Two ways to express single-valuedness of a class expression C ( y ) that is constant for those y e. B such that ph . The first antecedent ensures that the constant value belongs to the existential uniqueness domain A , and the second ensures that C ( y ) is evaluated for at least one y . (Contributed by NM, 4-Jan-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2 ( ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nfrab1 ⊢ Ⅎ 𝑦 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
2 nfcv ⊢ Ⅎ 𝑧 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
3 nfv ⊢ Ⅎ 𝑧 𝐶 ∈ 𝐴
4 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐶
5 4 nfel1 ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴
6 csbeq1a ⊢ ( 𝑦 = 𝑧 → 𝐶 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
7 6 eleq1d ⊢ ( 𝑦 = 𝑧 → ( 𝐶 ∈ 𝐴 ↔ ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ) )
8 1 2 3 5 7 cbvralfw ⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝐶 ∈ 𝐴 ↔ ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 )
9 rabid ⊢ ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
10 9 imbi1i ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝐶 ∈ 𝐴 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐶 ∈ 𝐴 ) )
11 impexp ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝐶 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝐶 ∈ 𝐴 ) ) )
12 10 11 bitri ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝐶 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝐶 ∈ 𝐴 ) ) )
13 12 ralbii2 ⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝐶 ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) )
14 8 13 bitr3i ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) )
15 rabn0 ⊢ ( { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝐵 𝜑 )
16 reusv2lem5 ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
17 nfv ⊢ Ⅎ 𝑧 𝑥 = 𝐶
18 4 nfeq2 ⊢ Ⅎ 𝑦 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶
19 6 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝐶 ↔ 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ) )
20 1 2 17 18 19 cbvrexfw ⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
21 9 anbi1i ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∧ 𝑥 = 𝐶 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) )
22 anass ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ∧ 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
23 21 22 bitri ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ∧ 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑥 = 𝐶 ) ) )
24 23 rexbii2 ⊢ ( ∃ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) )
25 20 24 bitr3i ⊢ ( ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) )
26 25 reubii ⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) )
27 1 2 17 18 19 cbvralfw ⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 )
28 9 imbi1i ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑥 = 𝐶 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝑥 = 𝐶 ) )
29 impexp ⊢ ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝑥 = 𝐶 ) ) )
30 28 29 bitri ⊢ ( ( 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } → 𝑥 = 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 → ( 𝜑 → 𝑥 = 𝐶 ) ) )
31 30 ralbii2 ⊢ ( ∀ 𝑦 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
32 27 31 bitr3i ⊢ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
33 32 reubii ⊢ ( ∃! 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } 𝑥 = ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
34 16 26 33 3bitr3g ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ⦋ 𝑧 / 𝑦 ⦌ 𝐶 ∈ 𝐴 ∧ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ≠ ∅ ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
35 14 15 34 syl2anbr ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝑥 = 𝐶 ) ↔ ∃! 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )