Theorem elintab 4918

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   ∈ wcel 2144  {cab 2738  Vcvv 3450  ∩ cint 4906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-int 4907

This theorem is used by:  elintrab  4919  intmin4  4936  intab  4937  dfom3  9651  dfom5  9654  tc2  9744  dfnn2  12351  brintclab  15159  efgi  19938  efgi2  19944  dfn0s2  28723  mclsax  36420  heibor1lem  38836  intabssd  44613  elmapintab  44689  cotrintab  44707  dffrege76  45032