Theorem rabbidv 3396

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rab 3390

This theorem is referenced by:  difeq2  4060  seex  5590  mptiniseg  6203  dfpred3g  6277  elovmporab  7613  elovmpt3rab1  7627  naddcllem  8612  naddov2  8615  naddcom  8618  naddrid  8619  naddass  8632  fineqvlem  9176  mapfien2  9322  supeq1  9358  supeq2  9361  supeq3  9362  oieq1  9427  oieq2  9428  ordtypecbv  9432  ordtypelem3  9435  harval  9475  inf3lema  9545  wemapwe  9618  oef1o  9619  tz9.12lem3  9713  rankvalb  9721  rankvalg  9741  ranksnb  9751  rankonidlem  9752  cardval3  9876  cardidm  9883  alephsuc2  10002  coftr  10195  fin1a2lem11  10332  fin1a2lem12  10333  hsmex  10354  axdc3lem2  10373  zorn2lem1  10418  zorn2lem6  10423  zorn2lem7  10424  zorn2g  10425  wuncval  10665  tskmval  10762  peano5uzti  12619  uzval  12790  rpnnen1  12933  ixxval  13306  fzval  13463  hashbclem  14414  hashbc  14415  shftfn  15035  bitsfval  16392  sadfval  16421  sadcom  16432  smufval  16446  smupp1  16449  smupval  16457  smumullem  16461  gcdval  16465  bezoutlem2  16509  bezoutlem4  16511  lcmval  16561  lcmfval  16590  lcmf0val  16591  lcmfpr  16596  isprm  16642  odzval  16762  pcval  16815  pceulem  16816  pceu  16817  pczpre  16818  pcdiv  16823  prmreclem1  16887  prmreclem4  16890  prmreclem5  16891  ramval  16979  cshws0  17072  imasdsval  17479  mrcval  17576  eldmcoa  18032  chneq1  18578  cycsubg2  19185  cntzval  19296  cntzsnval  19299  odfval  19507  odfvalALT  19508  odval  19509  gexval  19553  efgsfo  19714  dprdval  19980  ablfac1a  20046  ablfac1b  20047  ablfac1eu  20050  ablfaclem1  20062  ablfaclem3  20064  rnghmval  20420  rgspnval  20589  lspval  20970  ocvval  21647  dsmmelbas  21719  frlmsslss  21754  aspval  21852  psrass1lem  21912  psrmulval  21923  mplmonmul  22014  mhpval  22105  mhpmulcl  22115  coe1mul2  22234  pmatcoe1fsupp  22666  istopon  22877  toponsspwpw  22887  clsval  23002  neival  23067  ordtbaslem  23153  ordtbas2  23156  ordtopn1  23159  ordtopn2  23160  cnpval  23201  llyeq  23435  nllyeq  23436  ptfinfin  23484  finlocfin  23485  dissnlocfin  23494  locfindis  23495  xkoopn  23554  kqfval  23688  tsmsfbas  24093  blvalps  24350  blval  24351  nmofval  24679  nmoval  24680  ishtpy  24939  minveclem3b  25395  minveclem3  25396  minveclem4  25399  minveclem5  25400  ovolval  25440  vitalilem2  25576  vitalilem3  25577  vitalilem4  25578  vitali  25580  itg2monolem1  25717  elcpn  25901  mdegmullem  26043  elqaalem1  26285  elqaalem2  26286  elqaalem3  26287  elqaa  26288  aannenlem1  26294  aannenlem2  26295  jensen  26952  vmaval  27076  muval  27095  sgmval  27105  fsumdvdscom  27148  musum  27154  muinv  27156  dchrisum0fval  27468  dchrisum0ff  27470  logsqvma2  27506  pntrlog2bndlem1  27540  cutsval  27772  bdayons  28268  tglngval  28619  ttgval  28943  ttgitvval  28950  ebtwntg  29051  numedglnl  29213  dfnbgr2  29406  dfnbgr3  29407  uvtxusgr  29471  vtxdgval  29537  rusgrnumwrdl2  29655  iswwlksnon  29921  rusgrnumwwlks  30045  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwlknf1oclwwlknlem2  30152  clwwlknon  30160  clwwlk0on0  30162  eupth2  30309  fusgreg2wsplem  30403  fusgreghash2wsp  30408  numclwlk1lem1  30439  sspval  30794  ubthlem1  30941  ubthlem2  30942  ubthlem3  30943  ocval  31351  spanval  31404  chsupid  31483  eigvecval  31967  specval  31969  iunpreima  32634  fcobijfs2  32795  pwrssmgc  33060  fxpgaval  33228  nsgqusf1olem3  33475  mplvrpmrhm  33691  psrmonmul  33694  esplyfval  33707  esplyfval0  33708  minplyval  33849  constrsuc  33882  constrcbvlem  33899  crefeq  33989  zarcls1  34013  zarclsun  34014  zarclsiin  34015  zarclsint  34016  zarclssn  34017  zartop  34020  zartopon  34021  zart0  34023  zarmxt1  34024  zarcmp  34026  rhmpreimacnlem  34028  rhmpreimacn  34029  ordtcnvNEW  34064  ordtrest2NEW  34067  ordtconnlem1  34068  measvuni  34358  brfae  34392  omsfval  34438  orvcelval  34613  ballotlemi  34645  bnj602  35057  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  fineqvnttrclse  35268  onvf1odlem3  35287  subfacp1lem6  35367  kur14  35398  cvmscbv  35440  cvmsi  35447  cvmsval  35448  snmlval  35513  snmlflim  35514  satfv0  35540  satfv1  35545  satfv0fun  35553  satffunlem1lem1  35584  satffunlem2lem1  35586  satfv0fvfmla0  35595  satfv1fvfmla1  35605  prv1n  35613  fvray  36323  fwddifnval  36345  neibastop3  36544  weiunlem  36645  icoreval  37669  fin2so  37928  poimirlem26  37967  poimirlem27  37968  poimirlem28  37969  poimirlem32  37973  ftc1anclem6  38019  islinei  40186  pmapval  40203  paddval  40244  paddcom  40259  pclvalN  40336  ldilset  40555  dilsetN  40599  diafval  41477  diaval  41478  docavalN  41569  dicfval  41621  dochfval  41796  dochval  41797  mapdval  42074  mapdsn2  42088  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  prjcrvval  43065  2rexfrabdioph  43224  3rexfrabdioph  43225  4rexfrabdioph  43226  6rexfrabdioph  43227  7rexfrabdioph  43228  eldioph4i  43240  diophren  43241  pell1qrval  43274  pell14qrval  43276  pell1234qrval  43278  rpnnen3  43460  fnwe2lem1  43478  pwssplit4  43517  pwslnmlem2  43521  dgraaval  43572  itgoval  43589  proot1hash  43623  rp-intrabeq  43649  rp-unirabeq  43650  rfovfvd  44429  rfovfvfvd  44430  rfovcnvf1od  44431  fsovrfovd  44436  fsovfvd  44437  fsovfvfvd  44438  fsovcnvlem  44440  nzss  44744  supminfxr  45892  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  stoweidlem26  46454  stoweidlem27  46455  stoweidlem31  46459  stoweidlem34  46462  stoweidlem46  46474  fourierdlem79  46613  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem105  46639  fourierdlem107  46641  fourierdlem108  46642  fourierdlem110  46644  etransclem11  46673  salgenval  46749  subsaliuncl  46786  ovnval  46969  ovnval2  46973  ovnval2b  46980  ovncvrrp  46992  ovnsubaddlem1  46998  ovnsubadd  47000  ovncvr2  47039  hspmbl  47057  ovolval2  47072  ovnovollem3  47086  salpreimagelt  47135  salpreimalegt  47137  salpreimagtge  47153  salpreimaltle  47154  issmflem  47155  issmf  47156  salpreimagtlt  47158  smfpreimalt  47159  smfpreimaltf  47164  issmfle  47173  smfpimltxr  47175  smfpreimale  47182  issmfgt  47184  smfpreimagt  47190  issmfge  47198  smflimlem3  47201  smflimlem4  47202  smflim  47205  smfpimgtxr  47208  smfpreimage  47210  fvmptrabdm  47741  elsetpreimafveq  47857  prmdvdsfmtnof1  48050  fppr  48202  dfclnbgr2  48299  dfclnbgr3  48302  dfsclnbgr6  48334  grlimedgclnbgr  48471  grlimgrtri  48479  grilcbri2  48487  bigoval  49025  line  49208  rrxline  49210  sphere  49223  line2y  49231  inpw  49300