Theorem elintg 4845

Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003.) (Proof shortened by JJ, 26-Jul-2021.)

Assertion

Ref	Expression
elintg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem elintg

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2821	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
2	1	ralbidv 3110	. 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))
3		dfint2 4839	. 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥}
4	2, 3	elab2g 3576	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542   ∈ wcel 2114  ∀wral 3054  ∩ cint 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-int 4838

This theorem is referenced by:  elinti  4846  elrint  4880  onmindif  6262  onmindif2  7549  mremre  16981  toponmre  21847  1stcfb  22199  uffixfr  22677  plycpn  25040  insiga  31678  dfon2lem8  33343  elintabg  40750  trintALTVD  42061  trintALT  42062  elintd  42185  intsaluni  43433  intsal  43434