Theorem rabbi2dva 4148

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 3891	. 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵}
2		rabbi2dva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓))
3	2	rabbidva 3402	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝜓})
4	1, 3	eqtrid 2790	1 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {crab 3067   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3072  df-in 3890

This theorem is referenced by:  fndmdif  6901  bitsshft  16110  sylow3lem2  19148  leordtvallem1  22269  leordtvallem2  22270  ordtt1  22438  xkoccn  22678  txcnmpt  22683  xkopt  22714  ordthmeolem  22860  qustgphaus  23182  itg2monolem1  24820  lhop1  25083  efopn  25718  dirith  26582  pjvec  29959  pjocvec  29960  neibastop3  34478  diarnN  39070