Theorem eluniab 4923

Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)

Assertion

Ref	Expression
eluniab	⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eluniab

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eluni 4911	. 2 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}))
2		nfv 1917	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦
3		nfsab1 2717	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
4	2, 3	nfan 1902	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})
5		nfv 1917	. . 3 ⊢ Ⅎ𝑦(𝐴 ∈ 𝑥 ∧ 𝜑)
6		eleq2w 2817	. . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥))
7		eleq1w 2816	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}))
8		abid 2713	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	7, 8	bitrdi 286	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑))
10	6, 9	anbi12d 631	. . 3 ⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝑥 ∧ 𝜑)))
11	4, 5, 10	cbvexv1 2338	. 2 ⊢ (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
12	1, 11	bitri 274	1 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  {cab 2709  ∪ cuni 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-uni 4909

This theorem is referenced by:  elunirab  4924  dfiun2gOLD  5034  inuni  5343  elfv  6889  unielxp  8015  frrlem8  8280  frrlem10  8282  wfrlem12OLD  8322  tfrlem9  8387  dfac5lem2  10121  fin23lem30  10339  unisngl  23251  metrest  24253  aannenlem2  26066  fpwrelmapffslem  32212  dfiota3  35187  mptsnunlem  36522  nnoeomeqom  42364