Metamath Proof Explorer


Theorem dfiun2g

Description: Alternate definition of indexed union when B is a set. Definition 15(a) of Suppes p. 44. (Contributed by NM, 23-Mar-2006) (Proof shortened by Andrew Salmon, 25-Jul-2011) (Proof shortened by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Assertion dfiun2g ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )

Proof

Step Hyp Ref Expression
1 nfra1 𝑥𝑥𝐴 𝐵𝐶
2 rspa ( ( ∀ 𝑥𝐴 𝐵𝐶𝑥𝐴 ) → 𝐵𝐶 )
3 clel3g ( 𝐵𝐶 → ( 𝑧𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵𝑧𝑦 ) ) )
4 2 3 syl ( ( ∀ 𝑥𝐴 𝐵𝐶𝑥𝐴 ) → ( 𝑧𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵𝑧𝑦 ) ) )
5 1 4 rexbida ( ∀ 𝑥𝐴 𝐵𝐶 → ( ∃ 𝑥𝐴 𝑧𝐵 ↔ ∃ 𝑥𝐴𝑦 ( 𝑦 = 𝐵𝑧𝑦 ) ) )
6 rexcom4 ( ∃ 𝑥𝐴𝑦 ( 𝑦 = 𝐵𝑧𝑦 ) ↔ ∃ 𝑦𝑥𝐴 ( 𝑦 = 𝐵𝑧𝑦 ) )
7 5 6 bitrdi ( ∀ 𝑥𝐴 𝐵𝐶 → ( ∃ 𝑥𝐴 𝑧𝐵 ↔ ∃ 𝑦𝑥𝐴 ( 𝑦 = 𝐵𝑧𝑦 ) ) )
8 r19.41v ( ∃ 𝑥𝐴 ( 𝑦 = 𝐵𝑧𝑦 ) ↔ ( ∃ 𝑥𝐴 𝑦 = 𝐵𝑧𝑦 ) )
9 8 exbii ( ∃ 𝑦𝑥𝐴 ( 𝑦 = 𝐵𝑧𝑦 ) ↔ ∃ 𝑦 ( ∃ 𝑥𝐴 𝑦 = 𝐵𝑧𝑦 ) )
10 exancom ( ∃ 𝑦 ( ∃ 𝑥𝐴 𝑦 = 𝐵𝑧𝑦 ) ↔ ∃ 𝑦 ( 𝑧𝑦 ∧ ∃ 𝑥𝐴 𝑦 = 𝐵 ) )
11 9 10 bitri ( ∃ 𝑦𝑥𝐴 ( 𝑦 = 𝐵𝑧𝑦 ) ↔ ∃ 𝑦 ( 𝑧𝑦 ∧ ∃ 𝑥𝐴 𝑦 = 𝐵 ) )
12 7 11 bitrdi ( ∀ 𝑥𝐴 𝐵𝐶 → ( ∃ 𝑥𝐴 𝑧𝐵 ↔ ∃ 𝑦 ( 𝑧𝑦 ∧ ∃ 𝑥𝐴 𝑦 = 𝐵 ) ) )
13 eliun ( 𝑧 𝑥𝐴 𝐵 ↔ ∃ 𝑥𝐴 𝑧𝐵 )
14 eluniab ( 𝑧 { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ↔ ∃ 𝑦 ( 𝑧𝑦 ∧ ∃ 𝑥𝐴 𝑦 = 𝐵 ) )
15 12 13 14 3bitr4g ( ∀ 𝑥𝐴 𝐵𝐶 → ( 𝑧 𝑥𝐴 𝐵𝑧 { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } ) )
16 15 eqrdv ( ∀ 𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥𝐴 𝑦 = 𝐵 } )