Theorem elintg 4978

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 2832	. . 3 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥))
2	1	ralbidv 3184	. 2 ⊢ (𝑦 = 𝐴 → (∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))
3		dfint2 4972	. 2 ⊢ ∩ 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐵 𝑦 ∈ 𝑥}
4	2, 3	elab2g 3696	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ ∩ 𝐵 ↔ ∀𝑥 ∈ 𝐵 𝐴 ∈ 𝑥))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-int 4971

This theorem is referenced by:  elinti  4979  elintabg  4981  elrint  5013  onmindif  6487  onmindif2  7843  mremre  17662  toponmre  23122  1stcfb  23474  uffixfr  23952  plycpn  26349  insiga  34101  dfon2lem8  35754  trintALTVD  44851  trintALT  44852  elintd  44976  intsaluni  46250  intsal  46251