Theorem elintab 4914

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   ∈ wcel 2113  {cab 2714  Vcvv 3440  ∩ cint 4902

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-int 4903

This theorem is referenced by:  elintrab  4915  intmin4  4932  intab  4933  dfom3  9556  dfom5  9559  tc2  9649  dfnn2  12158  brintclab  14924  efgi  19648  efgi2  19654  dfn0s2  28328  mclsax  35763  heibor1lem  38006  intabssd  43756  elmapintab  43833  cotrintab  43851  dffrege76  44176