Theorem unir1 9671

Description: The cumulative hierarchy of sets covers the universe. Proposition 4.45 (b) to (a) of [Mendelson] p. 281. (Contributed by NM, 27-Sep-2004.) (Revised by Mario Carneiro, 8-Jun-2013.)

Assertion

Ref	Expression
unir1	⊢ ∪ (𝑅1 “ On) = V

Proof of Theorem unir1

Step	Hyp	Ref	Expression
1		setind 9592	. 2 ⊢ (∀𝑥(𝑥 ⊆ ∪ (𝑅1 “ On) → 𝑥 ∈ ∪ (𝑅1 “ On)) → ∪ (𝑅1 “ On) = V)
2		vex 3445	. . . 4 ⊢ 𝑥 ∈ V
3	2	r1elss 9664	. . 3 ⊢ (𝑥 ∈ ∪ (𝑅1 “ On) ↔ 𝑥 ⊆ ∪ (𝑅1 “ On))
4	3	biimpri 227	. 2 ⊢ (𝑥 ⊆ ∪ (𝑅1 “ On) → 𝑥 ∈ ∪ (𝑅1 “ On))
5	1, 4	mpg 1798	1 ⊢ ∪ (𝑅1 “ On) = V

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  Vcvv 3441   ⊆ wss 3898  ∪ cuni 4853   “ cima 5624  Oncon0 6303  𝑅₁cr1 9620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-reg 9450  ax-inf2 9499

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-ov 7341  df-om 7782  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-r1 9622

This theorem is referenced by:  jech9.3  9672  rankwflem  9673  rankval  9674  rankr1g  9690  rankid  9691  ssrankr1  9693  rankel  9697  rankval3  9698  rankpw  9701  rankss  9707  ranksn  9712  rankuni2  9713  rankun  9714  rankpr  9715  rankop  9716  r1rankid  9717  rankeq0  9719  rankr1b  9722  dfac12a  10006  hsmex2  10291  grutsk  10680  grurankcld  42224