Metamath Proof Explorer

Theorem reusv3

Description: Two ways to express single-valuedness of a class expression C ( y ) . See reusv1 for the connection to uniqueness. (Contributed by NM, 27-Dec-2012)

Ref Expression
Hypotheses reusv3.1 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
reusv3.2 ⊢ ( 𝑦 = 𝑧 → 𝐶 = 𝐷 )
Assertion reusv3 ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 reusv3.1 ⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
2 reusv3.2 ⊢ ( 𝑦 = 𝑧 → 𝐶 = 𝐷 )
3 2 eleq1d ⊢ ( 𝑦 = 𝑧 → ( 𝐶 ∈ 𝐴 ↔ 𝐷 ∈ 𝐴 ) )
4 1 3 anbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ↔ ( 𝜓 ∧ 𝐷 ∈ 𝐴 ) ) )
5 4 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) ↔ ∃ 𝑧 ∈ 𝐵 ( 𝜓 ∧ 𝐷 ∈ 𝐴 ) )
6 nfra2w ⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 )
7 nfv ⊢ Ⅎ 𝑧 ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 )
8 6 7 nfim ⊢ Ⅎ 𝑧 ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) )
9 risset ⊢ ( 𝐷 ∈ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐷 )
10 ralcom ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )
11 impexp ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ( 𝜑 → ( 𝜓 → 𝐶 = 𝐷 ) ) )
12 bi2.04 ⊢ ( ( 𝜑 → ( 𝜓 → 𝐶 = 𝐷 ) ) ↔ ( 𝜓 → ( 𝜑 → 𝐶 = 𝐷 ) ) )
13 11 12 bitri ⊢ ( ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ( 𝜓 → ( 𝜑 → 𝐶 = 𝐷 ) ) )
14 13 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( 𝜑 → 𝐶 = 𝐷 ) ) )
15 r19.21v ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝜓 → ( 𝜑 → 𝐶 = 𝐷 ) ) ↔ ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) )
16 14 15 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) )
17 16 ralbii ⊢ ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) )
18 10 17 bitri ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) )
19 rsp ⊢ ( ∀ 𝑧 ∈ 𝐵 ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) → ( 𝑧 ∈ 𝐵 → ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) ) )
20 18 19 sylbi ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ( 𝑧 ∈ 𝐵 → ( 𝜓 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) ) )
21 20 com3l ⊢ ( 𝑧 ∈ 𝐵 → ( 𝜓 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) ) )
22 21 imp31 ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ 𝜓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) )
23 eqeq1 ⊢ ( 𝑥 = 𝐷 → ( 𝑥 = 𝐶 ↔ 𝐷 = 𝐶 ) )
24 eqcom ⊢ ( 𝐷 = 𝐶 ↔ 𝐶 = 𝐷 )
25 23 24 bitrdi ⊢ ( 𝑥 = 𝐷 → ( 𝑥 = 𝐶 ↔ 𝐶 = 𝐷 ) )
26 25 imbi2d ⊢ ( 𝑥 = 𝐷 → ( ( 𝜑 → 𝑥 = 𝐶 ) ↔ ( 𝜑 → 𝐶 = 𝐷 ) ) )
27 26 ralbidv ⊢ ( 𝑥 = 𝐷 → ( ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝐶 = 𝐷 ) ) )
28 22 27 syl5ibrcom ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ 𝜓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ) → ( 𝑥 = 𝐷 → ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
29 28 reximdv ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ 𝜓 ) ∧ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐷 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
30 29 ex ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝜓 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐷 → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) ) )
31 30 com23 ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 = 𝐷 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) ) )
32 9 31 syl5bi ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝜓 ) → ( 𝐷 ∈ 𝐴 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) ) )
33 32 expimpd ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝜓 ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) ) )
34 8 33 rexlimi ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝜓 ∧ 𝐷 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
35 5 34 sylbi ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )
36 1 2 reusv3i ⊢ ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) )
37 35 36 impbid1 ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝜑 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( ( 𝜑 ∧ 𝜓 ) → 𝐶 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜑 → 𝑥 = 𝐶 ) ) )