Theorem rabbi2dva 4175

Description: Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)

Hypothesis

Ref	Expression
rabbi2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))

Assertion

Ref	Expression
rabbi2dva	⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓})

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem rabbi2dva

Step	Hyp	Ref	Expression
1		dfin5 3906	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
2		rabbi2dva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))
3	2	rabbidva 3402	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝜓})
4	1, 3	eqtrid 2780	1 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {crab 3396   ∩ cin 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-rab 3397  df-in 3905

This theorem is referenced by:  fndmdif  6983  bitsshft  16390  sylow3lem2  19544  leordtvallem1  23128  leordtvallem2  23129  ordtt1  23297  xkoccn  23537  txcnmpt  23542  xkopt  23573  ordthmeolem  23719  qustgphaus  24041  itg2monolem1  25681  lhop1  25949  efopn  26597  dirith  27470  pjvec  31680  pjocvec  31681  neibastop3  36429  diarnN  41251