Theorem elint2 4951

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1532   ∈ wcel 2099  ∀wral 3056  Vcvv 3469  ∩ cint 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-int 4945

This theorem is referenced by:  int0  4960  ssint  4962  intssuni  4968  iinuni  5095  onint  7787  intwun  10750  inttsk  10789  intgru  10829  subgint  19096  subrngint  20486  subrgint  20523  lssintcl  20837  toponmre  22984  alexsubALTlem3  23940  shintcli  31126  chintcli  31128  intlidl  33069  fin2so  37015  intidl  37437  mzpincl  42076  elimaint  43002  elintima  43006  intsal  45641  salgencntex  45654