Theorem elint2 3891

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1370   ∈ wcel 2175  ∀wral 2483  Vcvv 2771  ∩ cint 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773  df-int 3885

This theorem is referenced by:  elintg  3892  ssint  3900  intssunim  3906  iinuniss  4009  trint  4156  suplocexprlemmu  7830  suplocexprlemdisj  7832  suplocexprlemloc  7833  suplocexprlemub  7835