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

Metamath Proof Explorer

Theorem bnj1400

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1400.1 ⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
Assertion bnj1400 dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥

Proof

Step Hyp Ref Expression
1 bnj1400.1 ⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2 dmuni ⊢ dom ∪ 𝐴 = ∪ 𝑧 ∈ 𝐴 dom 𝑧
3 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 dom 𝑥 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 }
4 df-iun ⊢ ∪ 𝑧 ∈ 𝐴 dom 𝑧 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 }
5 1 nfcii ⊢ Ⅎ 𝑥 𝐴
6 nfcv ⊢ Ⅎ 𝑧 𝐴
7 nfv ⊢ Ⅎ 𝑧 𝑦 ∈ dom 𝑥
8 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ dom 𝑧
9 dmeq ⊢ ( 𝑥 = 𝑧 → dom 𝑥 = dom 𝑧 )
10 9 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ dom 𝑥 ↔ 𝑦 ∈ dom 𝑧 ) )
11 5 6 7 8 10 cbvrexfw ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 )
12 11 abbii ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 } = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ dom 𝑧 }
13 4 12 eqtr4i ⊢ ∪ 𝑧 ∈ 𝐴 dom 𝑧 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ dom 𝑥 }
14 3 13 eqtr4i ⊢ ∪ 𝑥 ∈ 𝐴 dom 𝑥 = ∪ 𝑧 ∈ 𝐴 dom 𝑧
15 2 14 eqtr4i ⊢ dom ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 dom 𝑥