Theorem elintab 4887

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
inteqab.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
elintab	⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elintab

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		inteqab.1	. . 3 ⊢ 𝐴 ∈ V
2	1	elint 4882	. 2 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦))
3		nfsab1 2723	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
4		nfv 1918	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦
5	3, 4	nfim 1900	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦)
6		nfv 1918	. . 3 ⊢ Ⅎ𝑦(𝜑 → 𝐴 ∈ 𝑥)
7		eleq1w 2821	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}))
8		abid 2719	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	7, 8	bitrdi 286	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑))
10		eleq2w 2822	. . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥))
11	9, 10	imbi12d 344	. . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ (𝜑 → 𝐴 ∈ 𝑥)))
12	5, 6, 11	cbvalv1 2340	. 2 ⊢ (∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
13	2, 12	bitri 274	1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2108  {cab 2715  Vcvv 3422  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-int 4877

This theorem is referenced by:  elintrab  4888  intmin4  4905  intab  4906  intid  5367  dfom3  9335  dfom5  9338  tc2  9431  dfnn2  11916  brintclab  14640  efgi  19240  efgi2  19246  mclsax  33431  heibor1lem  35894  intabssd  41024  elmapintab  41093  cotrintab  41111  dffrege76  41436