Theorem rabbi2dva 4247

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {crab 3443   ∩ cin 3975

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-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rab 3444  df-in 3983

This theorem is referenced by:  fndmdif  7075  bitsshft  16521  sylow3lem2  19670  leordtvallem1  23239  leordtvallem2  23240  ordtt1  23408  xkoccn  23648  txcnmpt  23653  xkopt  23684  ordthmeolem  23830  qustgphaus  24152  itg2monolem1  25805  lhop1  26073  efopn  26718  dirith  27591  pjvec  31728  pjocvec  31729  neibastop3  36328  diarnN  41086