Theorem elintab 4934

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

Hypothesis

Ref	Expression
elintab.ex	⊢ 𝐴 ∈ V

Assertion

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

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elintab

Step	Hyp	Ref	Expression
1		elintab.ex	. 2 ⊢ 𝐴 ∈ V
2		elintabg 4933	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  {cab 2713  Vcvv 3459  ∩ cint 4922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-int 4923

This theorem is referenced by:  elintrab  4936  intmin4  4953  intab  4954  intidOLD  5433  dfom3  9661  dfom5  9664  tc2  9756  dfnn2  12253  brintclab  15020  efgi  19700  efgi2  19706  dfn0s2  28276  mclsax  35591  heibor1lem  37833  intabssd  43543  elmapintab  43620  cotrintab  43638  dffrege76  43963