Theorem elintab 4787

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 4782	. 2 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦))
3		nfsab1 2782	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
4		nfv 1890	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦
5	3, 4	nfim 1876	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦)
6		nfv 1890	. . 3 ⊢ Ⅎ𝑦(𝜑 → 𝐴 ∈ 𝑥)
7		eleq1w 2863	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}))
8		abid 2777	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	7, 8	syl6bb 288	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑))
10		eleq2w 2864	. . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥))
11	9, 10	imbi12d 346	. . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ (𝜑 → 𝐴 ∈ 𝑥)))
12	5, 6, 11	cbvalv1 2318	. 2 ⊢ (∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
13	2, 12	bitri 276	1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1518   ∈ wcel 2079  {cab 2773  Vcvv 3432  ∩ cint 4776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-int 4777

This theorem is referenced by:  elintrab  4788  intmin4  4805  intab  4806  intid  5235  dfom3  8945  dfom5  8948  tc2  9019  dfnn2  11488  brintclab  14183  efgi  18560  efgi2  18566  mclsax  32369  heibor1lem  34565  intabssd  39321  elmapintab  39392  cotrintab  39410  dffrege76  39721