Theorem rabbidv 3480

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 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3478	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {crab 3142

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-rab 3147

This theorem is referenced by:  rabeqbidv  3485  difeq2  4093  seex  5518  mptiniseg  6093  dfpred3g  6159  elovmporab  7391  elovmpt3rab1  7405  suppcofnd  7871  fineqvlem  8732  mapfien2  8872  supeq1  8909  supeq2  8912  supeq3  8913  oieq1  8976  oieq2  8977  ordtypecbv  8981  ordtypelem3  8984  harval  9026  inf3lema  9087  wemapwe  9160  oef1o  9161  tz9.12lem3  9218  rankvalb  9226  rankvalg  9246  ranksnb  9256  rankonidlem  9257  cardval3  9381  cardidm  9388  alephsuc2  9506  coftr  9695  fin1a2lem11  9832  fin1a2lem12  9833  hsmex  9854  axdc3lem2  9873  zorn2lem1  9918  zorn2lem6  9923  zorn2lem7  9924  zorn2g  9925  wuncval  10164  tskmval  10261  peano5uzti  12073  uzval  12246  rpnnen1  12383  ixxval  12747  fzval  12895  hashbclem  13811  hashbc  13812  shftfn  14432  bitsfval  15772  sadfval  15801  sadcom  15812  smufval  15826  smupp1  15829  smupval  15837  smumullem  15841  gcdval  15845  bezoutlem2  15888  bezoutlem4  15890  lcmval  15936  lcmfval  15965  lcmf0val  15966  lcmfpr  15971  isprm  16017  odzval  16128  pcval  16181  pceulem  16182  pceu  16183  pczpre  16184  pcdiv  16189  prmreclem1  16252  prmreclem4  16255  prmreclem5  16256  ramval  16344  cshws0  16435  imasdsval  16788  mrcval  16881  eldmcoa  17325  cycsubg2  18353  cntzval  18451  cntzsnval  18454  odfval  18660  odfvalALT  18661  odval  18662  gexval  18703  efgsfo  18865  dprdval  19125  ablfac1a  19191  ablfac1b  19192  ablfac1eu  19195  ablfaclem1  19207  ablfaclem3  19209  lspval  19747  aspval  20102  psrass1lem  20157  psrmulval  20166  mplmonmul  20245  mhpval  20333  coe1mul2  20437  ocvval  20811  dsmmelbas  20883  frlmsslss  20918  pmatcoe1fsupp  21309  istopon  21520  toponsspwpw  21530  clsval  21645  neival  21710  ordtbaslem  21796  ordtbas2  21799  ordtopn1  21802  ordtopn2  21803  cnpval  21844  llyeq  22078  nllyeq  22079  ptfinfin  22127  finlocfin  22128  dissnlocfin  22137  locfindis  22138  xkoopn  22197  kqfval  22331  tsmsfbas  22736  blvalps  22995  blval  22996  nmofval  23323  nmoval  23324  ishtpy  23576  minveclem3b  24031  minveclem3  24032  minveclem4  24035  minveclem5  24036  ovolval  24074  vitalilem2  24210  vitalilem3  24211  vitalilem4  24212  vitali  24214  itg2monolem1  24351  elcpn  24531  mdegmullem  24672  elqaalem1  24908  elqaalem2  24909  elqaalem3  24910  elqaa  24911  aannenlem1  24917  aannenlem2  24918  jensen  25566  vmaval  25690  muval  25709  sgmval  25719  fsumdvdscom  25762  musum  25768  muinv  25770  dchrisum0fval  26081  dchrisum0ff  26083  logsqvma2  26119  pntrlog2bndlem1  26153  tglngval  26337  ttgval  26661  ttgitvval  26668  ebtwntg  26768  numedglnl  26929  dfnbgr2  27119  dfnbgr3  27120  uvtxusgr  27184  vtxdgval  27250  rusgrnumwrdl2  27368  iswwlksnon  27631  rusgrnumwwlks  27753  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwlknf1oclwwlknlem2  27861  clwwlknon  27869  clwwlk0on0  27871  eupth2  28018  fusgreg2wsplem  28112  fusgreghash2wsp  28117  numclwlk1lem1  28148  sspval  28500  ubthlem1  28647  ubthlem2  28648  ubthlem3  28649  ocval  29057  spanval  29110  chsupid  29189  eigvecval  29673  specval  29675  iunpreima  30316  crefeq  31109  ordtcnvNEW  31163  ordtrest2NEW  31166  ordtconnlem1  31167  measvuni  31473  brfae  31507  omsfval  31552  orvcelval  31726  ballotlemi  31758  bnj602  32187  subfacp1lem6  32432  kur14  32463  cvmscbv  32505  cvmsi  32512  cvmsval  32513  snmlval  32578  snmlflim  32579  satfv0  32605  satfv1  32610  satfv0fun  32618  satffunlem1lem1  32649  satffunlem2lem1  32651  satfv0fvfmla0  32660  satfv1fvfmla1  32670  prv1n  32678  scutval  33265  fvray  33602  fwddifnval  33624  neibastop3  33710  icoreval  34637  fin2so  34894  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem32  34939  ftc1anclem6  34987  islinei  36891  pmapval  36908  paddval  36949  paddcom  36964  pclvalN  37041  ldilset  37260  dilsetN  37304  diafval  38182  diaval  38183  docavalN  38274  dicfval  38326  dochfval  38501  dochval  38502  mapdval  38779  mapdsn2  38793  2rexfrabdioph  39413  3rexfrabdioph  39414  4rexfrabdioph  39415  6rexfrabdioph  39416  7rexfrabdioph  39417  eldioph4i  39429  diophren  39430  pell1qrval  39463  pell14qrval  39465  pell1234qrval  39467  rpnnen3  39649  fnwe2lem1  39670  pwssplit4  39709  pwslnmlem2  39713  dgraaval  39764  itgoval  39781  rgspnval  39788  proot1hash  39820  rfovfvd  40368  rfovfvfvd  40369  rfovcnvf1od  40370  fsovrfovd  40375  fsovfvd  40376  fsovfvfvd  40377  fsovcnvlem  40379  nzss  40669  supminfxr  41760  dvnprodlem1  42251  dvnprodlem2  42252  dvnprodlem3  42253  dvnprod  42254  stoweidlem26  42331  stoweidlem27  42332  stoweidlem31  42336  stoweidlem34  42339  stoweidlem46  42351  fourierdlem79  42490  fourierdlem96  42507  fourierdlem97  42508  fourierdlem98  42509  fourierdlem99  42510  fourierdlem105  42516  fourierdlem107  42518  fourierdlem108  42519  fourierdlem110  42521  etransclem11  42550  salgenval  42626  subsaliuncl  42661  ovnval  42843  ovnval2  42847  ovnval2b  42854  ovncvrrp  42866  ovnsubaddlem1  42872  ovnsubadd  42874  ovncvr2  42913  hspmbl  42931  ovolval2  42946  ovnovollem3  42960  salpreimagelt  43006  salpreimalegt  43008  salpreimagtge  43022  salpreimaltle  43023  issmflem  43024  issmf  43025  salpreimagtlt  43027  smfpreimalt  43028  smfpreimaltf  43033  issmfle  43042  smfpimltxr  43044  smfpreimale  43051  issmfgt  43053  smfpreimagt  43058  issmfge  43066  smflimlem3  43069  smflimlem4  43070  smflim  43073  smfpimgtxr  43076  smfpreimage  43078  fvmptrabdm  43512  elsetpreimafveq  43577  prmdvdsfmtnof1  43769  fppr  43911  rnghmval  44182  bigoval  44629  line  44739  rrxline  44741  sphere  44754  line2y  44762