Theorem elintab 4879

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 4874	. 2 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦))
3		nfsab1 2808	. . . 4 ⊢ Ⅎ𝑥 𝑦 ∈ {𝑥 ∣ 𝜑}
4		nfv 1911	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ 𝑦
5	3, 4	nfim 1893	. . 3 ⊢ Ⅎ𝑥(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦)
6		nfv 1911	. . 3 ⊢ Ⅎ𝑦(𝜑 → 𝐴 ∈ 𝑥)
7		eleq1w 2895	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑥 ∈ {𝑥 ∣ 𝜑}))
8		abid 2803	. . . . 5 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	7, 8	syl6bb 289	. . . 4 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑))
10		eleq2w 2896	. . . 4 ⊢ (𝑦 = 𝑥 → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥))
11	9, 10	imbi12d 347	. . 3 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ (𝜑 → 𝐴 ∈ 𝑥)))
12	5, 6, 11	cbvalv1 2357	. 2 ⊢ (∀𝑦(𝑦 ∈ {𝑥 ∣ 𝜑} → 𝐴 ∈ 𝑦) ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))
13	2, 12	bitri 277	1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1531   ∈ wcel 2110  {cab 2799  Vcvv 3494  ∩ cint 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-int 4869

This theorem is referenced by:  elintrab  4880  intmin4  4897  intab  4898  intid  5342  dfom3  9104  dfom5  9107  tc2  9178  dfnn2  11645  brintclab  14355  efgi  18839  efgi2  18845  mclsax  32811  heibor1lem  35081  intabssd  39878  elmapintab  39949  cotrintab  39967  dffrege76  40278