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 𝑥