Theorem elintab 4938

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537   ∈ wcel 2107  {cab 2712  Vcvv 3463  ∩ cint 4926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-int 4927

This theorem is referenced by:  elintrab  4940  intmin4  4957  intab  4958  intidOLD  5443  dfom3  9669  dfom5  9672  tc2  9764  dfnn2  12261  brintclab  15023  efgi  19706  efgi2  19712  dfn0s2  28273  mclsax  35549  heibor1lem  37791  intabssd  43509  elmapintab  43586  cotrintab  43604  dffrege76  43929