Theorem uniexr 7784

Description: Converse of the Axiom of Union. Note that it does not require ax-un 7758. (Contributed by NM, 11-Nov-2003.)

Assertion

Ref	Expression
uniexr	⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V)

Proof of Theorem uniexr

Step	Hyp	Ref	Expression
1		pwuni 4908	. 2 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴
2		pwexg 5343	. 2 ⊢ (∪ 𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴 ∈ V)
3		ssexg 5284	. 2 ⊢ ((𝐴 ⊆ 𝒫 ∪ 𝐴 ∧ 𝒫 ∪ 𝐴 ∈ V) → 𝐴 ∈ V)
4	1, 2, 3	sylancr 599	1 ⊢ (∪ 𝐴 ∈ 𝑉 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3453   ⊆ wss 3899  𝒫 cpw 4559  ∪ cuni 4869

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251  ax-pow 5330

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-in 4093  df-pw 4561  df-uni 4870

This theorem is used by:  uniexb  7785  ssonprc  7808  ac5num  10125  bj-restv  38155  bj-mooreset  38162  ipoglb0  50247