Metamath Proof Explorer

Theorem eusvobj2

Description: Specify the same property in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis eusvobj1.1 ⊢ 𝐵 ∈ V
Assertion eusvobj2 ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eusvobj1.1 ⊢ 𝐵 ∈ V
2 euabsn2 ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∃ 𝑧 { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } )
3 eleq2 ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } ↔ 𝑥 ∈ { 𝑧 } ) )
4 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } ↔ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
5 velsn ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
6 3 4 5 3bitr3g ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ 𝑥 = 𝑧 ) )
7 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵
8 7 nfab ⊢ Ⅎ 𝑦 { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 }
9 8 nfeq1 ⊢ Ⅎ 𝑦 { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 }
10 1 elabrex ⊢ ( 𝑦 ∈ 𝐴 → 𝐵 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } )
11 eleq2 ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( 𝐵 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } ↔ 𝐵 ∈ { 𝑧 } ) )
12 1 elsn ⊢ ( 𝐵 ∈ { 𝑧 } ↔ 𝐵 = 𝑧 )
13 eqcom ⊢ ( 𝐵 = 𝑧 ↔ 𝑧 = 𝐵 )
14 12 13 bitri ⊢ ( 𝐵 ∈ { 𝑧 } ↔ 𝑧 = 𝐵 )
15 11 14 bitrdi ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( 𝐵 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } ↔ 𝑧 = 𝐵 ) )
16 10 15 syl5ib ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( 𝑦 ∈ 𝐴 → 𝑧 = 𝐵 ) )
17 9 16 ralrimi ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 )
18 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐵 ↔ 𝑧 = 𝐵 ) )
19 18 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑧 = 𝐵 ) )
20 17 19 syl5ibrcom ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( 𝑥 = 𝑧 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
21 6 20 sylbid ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
22 21 exlimiv ⊢ ( ∃ 𝑧 { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 } = { 𝑧 } → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
23 2 22 sylbi ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
24 euex ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
25 rexn0 ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝐴 ≠ ∅ )
26 25 exlimiv ⊢ ( ∃ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → 𝐴 ≠ ∅ )
27 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 )
28 27 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
29 24 26 28 3syl ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )
30 23 29 impbid ⊢ ( ∃! 𝑥 ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 = 𝐵 ) )