Theorem rabbidv 2804

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)

Hypothesis

Ref	Expression
rabbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 2803	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398   ∈ wcel 2205  {crab 2526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-ral 2527  df-rab 2531

This theorem is referenced by:  rabeqbidv  2810  difeq2  3333  seex  4458  mptiniseg  5259  elovmporab  6256  supeq1  7279  supeq2  7282  supeq3  7283  cardcl  7479  isnumi  7480  cardval3ex  7483  carden2bex  7488  genpdflem  7827  genipv  7829  genpelxp  7831  addcomprg  7898  mulcomprg  7900  uzval  9861  ixxval  10235  fzval  10350  hashinfom  11149  hashennn  11151  ssenneg  11212  hashfibclem  11214  hashfibc  11215  shftfn  11517  bitsfval  12636  gcdval  12663  lcmval  12768  isprm  12814  odzval  12947  pceulem  13000  pceu  13001  pcval  13002  pczpre  13003  pcdiv  13008  lspval  14587  istopon  14927  toponsspwpwg  14936  clsval  15025  neival  15057  cnpval  15112  blvalps  15302  blval  15303  limccl  15573  ellimc3apf  15574  eldvap  15596  sgmval  15900  vtxdgfifival  16335  clwwlknon  16473  clwwlk0on0  16475  eupth2fi  16523