Theorem rabbidv 3402

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 3401	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2111  {crab 3395

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-rab 3396

This theorem is referenced by:  difeq2  4070  seex  5575  mptiniseg  6186  dfpred3g  6260  elovmporab  7592  elovmpt3rab1  7606  naddcllem  8591  naddov2  8594  naddcom  8597  naddrid  8598  naddass  8611  fineqvlem  9150  mapfien2  9293  supeq1  9329  supeq2  9332  supeq3  9333  oieq1  9398  oieq2  9399  ordtypecbv  9403  ordtypelem3  9406  harval  9446  inf3lema  9514  wemapwe  9587  oef1o  9588  tz9.12lem3  9679  rankvalb  9687  rankvalg  9707  ranksnb  9717  rankonidlem  9718  cardval3  9842  cardidm  9849  alephsuc2  9968  coftr  10161  fin1a2lem11  10298  fin1a2lem12  10299  hsmex  10320  axdc3lem2  10339  zorn2lem1  10384  zorn2lem6  10389  zorn2lem7  10390  zorn2g  10391  wuncval  10630  tskmval  10727  peano5uzti  12560  uzval  12731  rpnnen1  12878  ixxval  13250  fzval  13406  hashbclem  14356  hashbc  14357  shftfn  14977  bitsfval  16331  sadfval  16360  sadcom  16371  smufval  16385  smupp1  16388  smupval  16396  smumullem  16400  gcdval  16404  bezoutlem2  16448  bezoutlem4  16450  lcmval  16500  lcmfval  16529  lcmf0val  16530  lcmfpr  16535  isprm  16581  odzval  16700  pcval  16753  pceulem  16754  pceu  16755  pczpre  16756  pcdiv  16761  prmreclem1  16825  prmreclem4  16828  prmreclem5  16829  ramval  16917  cshws0  17010  imasdsval  17416  mrcval  17513  eldmcoa  17969  chneq1  18515  cycsubg2  19120  cntzval  19231  cntzsnval  19234  odfval  19442  odfvalALT  19443  odval  19444  gexval  19488  efgsfo  19649  dprdval  19915  ablfac1a  19981  ablfac1b  19982  ablfac1eu  19985  ablfaclem1  19997  ablfaclem3  19999  rnghmval  20356  rgspnval  20525  lspval  20906  ocvval  21602  dsmmelbas  21674  frlmsslss  21709  aspval  21808  psrass1lem  21867  psrmulval  21879  mplmonmul  21969  mhpval  22052  mhpmulcl  22062  coe1mul2  22181  pmatcoe1fsupp  22614  istopon  22825  toponsspwpw  22835  clsval  22950  neival  23015  ordtbaslem  23101  ordtbas2  23104  ordtopn1  23107  ordtopn2  23108  cnpval  23149  llyeq  23383  nllyeq  23384  ptfinfin  23432  finlocfin  23433  dissnlocfin  23442  locfindis  23443  xkoopn  23502  kqfval  23636  tsmsfbas  24041  blvalps  24298  blval  24299  nmofval  24627  nmoval  24628  ishtpy  24896  minveclem3b  25353  minveclem3  25354  minveclem4  25357  minveclem5  25358  ovolval  25399  vitalilem2  25535  vitalilem3  25536  vitalilem4  25537  vitali  25539  itg2monolem1  25676  elcpn  25861  mdegmullem  26008  elqaalem1  26252  elqaalem2  26253  elqaalem3  26254  elqaa  26255  aannenlem1  26261  aannenlem2  26262  jensen  26924  vmaval  27048  muval  27067  sgmval  27077  fsumdvdscom  27120  musum  27126  muinv  27128  dchrisum0fval  27441  dchrisum0ff  27443  logsqvma2  27479  pntrlog2bndlem1  27513  scutval  27739  bdayon  28207  tglngval  28527  ttgval  28851  ttgitvval  28858  ebtwntg  28958  numedglnl  29120  dfnbgr2  29313  dfnbgr3  29314  uvtxusgr  29378  vtxdgval  29445  rusgrnumwrdl2  29563  iswwlksnon  29829  rusgrnumwwlks  29950  hashecclwwlkn1  30052  umgrhashecclwwlk  30053  clwlknf1oclwwlknlem2  30057  clwwlknon  30065  clwwlk0on0  30067  eupth2  30214  fusgreg2wsplem  30308  fusgreghash2wsp  30313  numclwlk1lem1  30344  sspval  30698  ubthlem1  30845  ubthlem2  30846  ubthlem3  30847  ocval  31255  spanval  31308  chsupid  31387  eigvecval  31871  specval  31873  iunpreima  32539  fcobijfs2  32700  pwrssmgc  32976  fxpgaval  33131  nsgqusf1olem3  33375  mplvrpmrhm  33572  esplyfval  33581  minplyval  33713  constrsuc  33746  constrcbvlem  33763  crefeq  33853  zarcls1  33877  zarclsun  33878  zarclsiin  33879  zarclsint  33880  zarclssn  33881  zartop  33884  zartopon  33885  zart0  33887  zarmxt1  33888  zarcmp  33890  rhmpreimacnlem  33892  rhmpreimacn  33893  ordtcnvNEW  33928  ordtrest2NEW  33931  ordtconnlem1  33932  measvuni  34222  brfae  34256  omsfval  34302  orvcelval  34477  ballotlemi  34509  bnj602  34922  fineqvnttrclselem2  35130  fineqvnttrclselem3  35131  fineqvnttrclse  35132  onvf1odlem3  35137  subfacp1lem6  35217  kur14  35248  cvmscbv  35290  cvmsi  35297  cvmsval  35298  snmlval  35363  snmlflim  35364  satfv0  35390  satfv1  35395  satfv0fun  35403  satffunlem1lem1  35434  satffunlem2lem1  35436  satfv0fvfmla0  35445  satfv1fvfmla1  35455  prv1n  35463  fvray  36174  fwddifnval  36196  neibastop3  36395  weiunlem2  36496  icoreval  37386  fin2so  37646  poimirlem26  37685  poimirlem27  37686  poimirlem28  37687  poimirlem32  37691  ftc1anclem6  37737  islinei  39778  pmapval  39795  paddval  39836  paddcom  39851  pclvalN  39928  ldilset  40147  dilsetN  40191  diafval  41069  diaval  41070  docavalN  41161  dicfval  41213  dochfval  41388  dochval  41389  mapdval  41666  mapdsn2  41680  grpods  42226  unitscyglem1  42227  unitscyglem2  42228  unitscyglem3  42229  unitscyglem4  42230  prjcrvval  42664  2rexfrabdioph  42828  3rexfrabdioph  42829  4rexfrabdioph  42830  6rexfrabdioph  42831  7rexfrabdioph  42832  eldioph4i  42844  diophren  42845  pell1qrval  42878  pell14qrval  42880  pell1234qrval  42882  rpnnen3  43064  fnwe2lem1  43082  pwssplit4  43121  pwslnmlem2  43125  dgraaval  43176  itgoval  43193  proot1hash  43227  rp-intrabeq  43253  rp-unirabeq  43254  rfovfvd  44034  rfovfvfvd  44035  rfovcnvf1od  44036  fsovrfovd  44041  fsovfvd  44042  fsovfvfvd  44043  fsovcnvlem  44045  nzss  44349  supminfxr  45501  dvnprodlem1  45983  dvnprodlem2  45984  dvnprodlem3  45985  dvnprod  45986  stoweidlem26  46063  stoweidlem27  46064  stoweidlem31  46068  stoweidlem34  46071  stoweidlem46  46083  fourierdlem79  46222  fourierdlem96  46239  fourierdlem97  46240  fourierdlem98  46241  fourierdlem99  46242  fourierdlem105  46248  fourierdlem107  46250  fourierdlem108  46251  fourierdlem110  46253  etransclem11  46282  salgenval  46358  subsaliuncl  46395  ovnval  46578  ovnval2  46582  ovnval2b  46589  ovncvrrp  46601  ovnsubaddlem1  46607  ovnsubadd  46609  ovncvr2  46648  hspmbl  46666  ovolval2  46681  ovnovollem3  46695  salpreimagelt  46744  salpreimalegt  46746  salpreimagtge  46762  salpreimaltle  46763  issmflem  46764  issmf  46765  salpreimagtlt  46767  smfpreimalt  46768  smfpreimaltf  46773  issmfle  46782  smfpimltxr  46784  smfpreimale  46791  issmfgt  46793  smfpreimagt  46799  issmfge  46807  smflimlem3  46810  smflimlem4  46811  smflim  46814  smfpimgtxr  46817  smfpreimage  46819  fvmptrabdm  47323  elsetpreimafveq  47427  prmdvdsfmtnof1  47617  fppr  47756  dfclnbgr2  47853  dfclnbgr3  47856  dfsclnbgr6  47888  grlimedgclnbgr  48025  grlimgrtri  48033  grilcbri2  48041  bigoval  48580  line  48763  rrxline  48765  sphere  48778  line2y  48786  inpw  48855