Theorem elint2 4886

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 4885	. 2 ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
3		df-ral 3069	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥))
4	2, 3	bitr4i 277	1 ⊢ (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   ∈ wcel 2106  ∀wral 3064  Vcvv 3432  ∩ cint 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-int 4880

This theorem is referenced by:  int0  4893  ssint  4895  intssuni  4901  iinuni  5027  onint  7640  intwun  10491  inttsk  10530  intgru  10570  subgint  18779  subrgint  20046  lssintcl  20226  toponmre  22244  alexsubALTlem3  23200  shintcli  29691  chintcli  29693  intlidl  31602  fin2so  35764  intidl  36187  mzpincl  40556  elimaint  41257  elintima  41261  intsal  43869  salgencntex  43882