Theorem elintab 4909

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 4908	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥)))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ ∩ {𝑥 ∣ 𝜑} ↔ ∀𝑥(𝜑 → 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2111  {cab 2709  Vcvv 3436  ∩ cint 4897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-int 4898

This theorem is referenced by:  elintrab  4910  intmin4  4927  intab  4928  dfom3  9537  dfom5  9540  tc2  9630  dfnn2  12138  brintclab  14908  efgi  19632  efgi2  19638  dfn0s2  28261  mclsax  35611  heibor1lem  37855  intabssd  43558  elmapintab  43635  cotrintab  43653  dffrege76  43978