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 
|- ( y e. A -> A. x y e. A )
Assertion bnj1400 
|- dom U. A = U_ x e. A dom x

Proof

Step Hyp Ref Expression
1 bnj1400.1 
 |-  ( y e. A -> A. x y e. A )
2 dmuni 
 |-  dom U. A = U_ z e. A dom z
3 df-iun 
 |-  U_ x e. A dom x = { y | E. x e. A y e. dom x }
4 df-iun 
 |-  U_ z e. A dom z = { y | E. z e. A y e. dom z }
5 1 nfcii 
 |-  F/_ x A
6 nfcv 
 |-  F/_ z A
7 nfv 
 |-  F/ z y e. dom x
8 nfv 
 |-  F/ x y e. dom z
9 dmeq 
 |-  ( x = z -> dom x = dom z )
10 9 eleq2d 
 |-  ( x = z -> ( y e. dom x <-> y e. dom z ) )
11 5 6 7 8 10 cbvrexfw 
 |-  ( E. x e. A y e. dom x <-> E. z e. A y e. dom z )
12 11 abbii 
 |-  { y | E. x e. A y e. dom x } = { y | E. z e. A y e. dom z }
13 4 12 eqtr4i 
 |-  U_ z e. A dom z = { y | E. x e. A y e. dom x }
14 3 13 eqtr4i 
 |-  U_ x e. A dom x = U_ z e. A dom z
15 2 14 eqtr4i 
 |-  dom U. A = U_ x e. A dom x