Theorem eluniab 4881

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 4870	. 2 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}))
2		nfv 1947	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦
3		nfsab1 2746	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
4	2, 3	nfan 1932	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑})
5		nfv 1947	. . 3 ⊢ Ⅎ𝑦(𝐴 ∈ 𝑥 ∧ 𝜑)
6		eleq2w 2844	. . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥))
7		eleq1w 2843	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}))
8		abid 2742	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	7, 8	bitrdi 290	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑))
10	6, 9	anbi12d 644	. . 3 ⊢ (𝑦 = 𝑥 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝐴 ∈ 𝑥 ∧ 𝜑)))
11	4, 5, 10	cbvexv1 2371	. 2 ⊢ (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))
12	1, 11	bitri 278	1 ⊢ (𝐴 ∈ ∪ {𝑥 ∣ 𝜑} ↔ ∃𝑥(𝐴 ∈ 𝑥 ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  {cab 2738  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-uni 4868

This theorem is used by:  elunirab  4882  inuni  5314  elfv  6876  unielxp  8024  frrlem8  8292  frrlem10  8294  tfrlem9  8374  dfac5lem2  10127  fin23lem30  10344  unisngl  23753  metrest  24750  aannenlem2  26565  fpwrelmapffslem  33203  dfiota3  36500  mptsnunlem  38092  nnoeomeqom  44153