Theorem elint2 4923

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999.)

Hypothesis

Ref	Expression
elint2.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
elint2	⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elint2

Step	Hyp	Ref	Expression
1		elint2.1	. . 3 ⊢ 𝐴 ∈ V
2	1	elint 4922	. 2 ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
3		df-ral 3086	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
4	2, 3	bitr4i 281	1 ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   ∈ wcel 2149  ∀wral 3085  Vcvv 3463  ∩ cint 4916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-int 4917

This theorem is referenced by:  int0  4931  ssint  4933  intssuni  4939  iinuni  5068  onint  7789  intwun  10720  inttsk  10759  intgru  10799  subgint  19217  subrngint  20645  subrgint  20680  lssintcl  21063  toponmre  23219  alexsubALTlem3  24175  shintcli  31622  chintcli  31624  intlidl  33672  fin2so  38146  intidl  38568  mzpincl  43357  elimaint  44267  elintima  44271  intsal  46936  salgencntex  46949