Theorem rabbidv 3400

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ∈ wcel 2121  {crab 3393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-rab 3394

This theorem is referenced by:  difeq2  4053  seex  5579  mptiniseg  6193  dfpred3g  6267  elovmporab  7605  elovmpt3rab1  7619  naddcllem  8606  naddov2  8609  naddcom  8612  naddrid  8613  naddass  8626  fineqvlem  9170  mapfien2  9316  supeq1  9352  supeq2  9355  supeq3  9356  oieq1  9421  oieq2  9422  ordtypecbv  9426  ordtypelem3  9429  harval  9469  inf3lema  9540  wemapwe  9613  oef1o  9614  tz9.12lem3  9708  rankvalb  9716  rankvalg  9736  ranksnb  9746  rankonidlem  9747  cardval3  9871  cardidm  9878  alephsuc2  9997  coftr  10191  fin1a2lem11  10328  fin1a2lem12  10329  hsmex  10350  axdc3lem2  10369  zorn2lem1  10414  zorn2lem6  10419  zorn2lem7  10420  zorn2g  10421  wuncval  10661  tskmval  10758  peano5uzti  12614  uzval  12785  rpnnen1  12928  ixxval  13301  fzval  13458  hashbclem  14409  hashbc  14410  shftfn  15030  bitsfval  16387  sadfval  16416  sadcom  16427  smufval  16441  smupp1  16444  smupval  16452  smumullem  16456  gcdval  16460  bezoutlem2  16504  bezoutlem4  16506  lcmval  16556  lcmfval  16585  lcmf0val  16586  lcmfpr  16591  isprm  16637  odzval  16757  pcval  16810  pceulem  16811  pceu  16812  pczpre  16813  pcdiv  16818  prmreclem1  16882  prmreclem4  16885  prmreclem5  16886  ramval  16974  cshws0  17067  imasdsval  17474  mrcval  17571  eldmcoa  18027  chneq1  18573  cycsubg2  19180  cntzval  19290  cntzsnval  19293  odfval  19501  odfvalALT  19502  odval  19503  gexval  19547  efgsfo  19708  dprdval  19974  ablfac1a  20040  ablfac1b  20041  ablfac1eu  20044  ablfaclem1  20056  ablfaclem3  20058  rnghmval  20414  rgspnval  20587  lspval  20968  ocvval  21645  dsmmelbas  21717  frlmsslss  21752  aspval  21850  psrass1lem  21911  psrmulval  21922  mplmonmul  22015  mhpval  22130  mhpmulcl  22140  coe1mul2  22258  pmatcoe1fsupp  22687  istopon  22898  toponsspwpw  22908  clsval  23023  neival  23088  ordtbaslem  23174  ordtbas2  23177  ordtopn1  23180  ordtopn2  23181  cnpval  23222  llyeq  23456  nllyeq  23457  ptfinfin  23505  finlocfin  23506  dissnlocfin  23515  locfindis  23516  xkoopn  23575  kqfval  23709  tsmsfbas  24114  blvalps  24371  blval  24372  nmofval  24700  nmoval  24701  ishtpy  24960  minveclem3b  25416  minveclem3  25417  minveclem4  25420  minveclem5  25421  ovolval  25461  vitalilem2  25597  vitalilem3  25598  vitalilem4  25599  vitali  25601  itg2monolem1  25738  elcpn  25922  mdegmullem  26064  elqaalem1  26306  elqaalem2  26307  elqaalem3  26308  elqaa  26309  aannenlem1  26315  aannenlem2  26316  jensen  26973  vmaval  27097  muval  27116  sgmval  27126  fsumdvdscom  27169  musum  27175  muinv  27177  dchrisum0fval  27489  dchrisum0ff  27491  logsqvma2  27527  pntrlog2bndlem1  27561  cutsval  27792  bdayons  28288  tglngval  28639  ttgval  28963  ttgitvval  28970  ebtwntg  29071  numedglnl  29233  dfnbgr2  29426  dfnbgr3  29427  uvtxusgr  29491  vtxdgval  29557  rusgrnumwrdl2  29675  iswwlksnon  29941  rusgrnumwwlks  30065  hashecclwwlkn1  30167  umgrhashecclwwlk  30168  clwlknf1oclwwlknlem2  30172  clwwlknon  30180  clwwlk0on0  30182  eupth2  30329  fusgreg2wsplem  30423  fusgreghash2wsp  30428  numclwlk1lem1  30459  sspval  30814  ubthlem1  30961  ubthlem2  30962  ubthlem3  30963  ocval  31371  spanval  31424  chsupid  31503  eigvecval  31987  specval  31989  iunpreima  32655  fcobijfs2  32816  pwrssmgc  33081  fxpgaval  33250  nsgqusf1olem3  33500  selvply1rhmlemb  33713  mplvrpmrhm  33741  psrmonmul  33744  esplyfval  33757  esplyfval0  33758  minplyval  33899  constrsuc  33932  constrcbvlem  33949  crefeq  34039  zarcls1  34063  zarclsun  34064  zarclsiin  34065  zarclsint  34066  zarclssn  34067  zartop  34070  zartopon  34071  zart0  34073  zarmxt1  34074  zarcmp  34076  rhmpreimacnlem  34078  rhmpreimacn  34079  ordtcnvNEW  34114  ordtrest2NEW  34117  ordtconnlem1  34118  measvuni  34408  brfae  34442  omsfval  34488  orvcelval  34663  ballotlemi  34695  bnj602  35110  fineqvnttrclselem2  35316  fineqvnttrclselem3  35317  fineqvnttrclse  35318  onvf1odlem3  35346  subfacp1lem6  35426  kur14  35457  cvmscbv  35499  cvmsi  35506  cvmsval  35507  snmlval  35572  snmlflim  35573  satfv0  35599  satfv1  35604  satfv0fun  35612  satffunlem1lem1  35643  satffunlem2lem1  35645  satfv0fvfmla0  35654  satfv1fvfmla1  35664  prv1n  35672  fvray  36382  fwddifnval  36404  neibastop3  36603  weiunlem  36704  icoreval  37728  fin2so  37987  poimirlem26  38026  poimirlem27  38027  poimirlem28  38028  poimirlem32  38032  ftc1anclem6  38078  islinei  40245  pmapval  40262  paddval  40303  paddcom  40318  pclvalN  40395  ldilset  40614  dilsetN  40658  diafval  41536  diaval  41537  docavalN  41628  dicfval  41680  dochfval  41855  dochval  41856  mapdval  42133  mapdsn2  42147  grpods  42692  unitscyglem1  42693  unitscyglem2  42694  unitscyglem3  42695  unitscyglem4  42696  prjcrvval  43095  2rexfrabdioph  43254  3rexfrabdioph  43255  4rexfrabdioph  43256  6rexfrabdioph  43257  7rexfrabdioph  43258  eldioph4i  43270  diophren  43271  pell1qrval  43304  pell14qrval  43306  pell1234qrval  43308  rpnnen3  43490  fnwe2lem1  43508  pwssplit4  43547  pwslnmlem2  43551  dgraaval  43602  itgoval  43619  proot1hash  43653  rp-intrabeq  43679  rp-unirabeq  43680  rfovfvd  44459  rfovfvfvd  44460  rfovcnvf1od  44461  fsovrfovd  44466  fsovfvd  44467  fsovfvfvd  44468  fsovcnvlem  44470  nzss  44774  supminfxr  45919  dvnprodlem1  46401  dvnprodlem2  46402  dvnprodlem3  46403  dvnprod  46404  stoweidlem26  46481  stoweidlem27  46482  stoweidlem31  46486  stoweidlem34  46489  stoweidlem46  46501  fourierdlem79  46640  fourierdlem96  46657  fourierdlem97  46658  fourierdlem98  46659  fourierdlem99  46660  fourierdlem105  46666  fourierdlem107  46668  fourierdlem108  46669  fourierdlem110  46671  etransclem11  46700  salgenval  46776  subsaliuncl  46813  ovnval  46996  ovnval2  47000  ovnval2b  47007  ovncvrrp  47019  ovnsubaddlem1  47025  ovnsubadd  47027  ovncvr2  47066  hspmbl  47084  ovolval2  47099  ovnovollem3  47113  salpreimagelt  47162  salpreimalegt  47164  salpreimagtge  47180  salpreimaltle  47181  issmflem  47182  issmf  47183  salpreimagtlt  47185  smfpreimalt  47186  smfpreimaltf  47191  issmfle  47200  smfpimltxr  47202  smfpreimale  47209  issmfgt  47211  smfpreimagt  47217  issmfge  47225  smflimlem3  47228  smflimlem4  47229  smflim  47232  smfpimgtxr  47235  smfpreimage  47237  fvmptrabdm  47768  elsetpreimafveq  47884  prmdvdsfmtnof1  48077  fppr  48229  dfclnbgr2  48326  dfclnbgr3  48329  dfsclnbgr6  48361  grlimedgclnbgr  48498  grlimgrtri  48506  grilcbri2  48514  bigoval  49052  line  49235  rrxline  49237  sphere  49250  line2y  49258  inpw  49327