Theorem rabbidv 3423

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-rab 3417

This theorem is used by:  difeq2  4060  seex  5615  mptiniseg  6254  dfpred3g  6337  iunpreima  7095  elovmporab  7694  elovmpt3rab1  7708  fnwe2lem2  8176  naddcllem  8716  naddov2  8719  naddcom  8723  naddrid  8724  naddass  8737  fineqvlem  9288  mapfien2  9431  supeq1  9467  supeq2  9470  supeq3  9471  oieq1  9536  oieq2  9537  ordtypecbv  9541  ordtypelem3  9544  harval  9584  inf3lema  9655  wemapwe  9728  oef1o  9729  tz9.12lem3  9826  rankvalb  9835  rankvalg  9856  ranksnb  9867  rankonidlem  9868  cardval3  10063  cardidm  10070  alephsuc2  10189  coftr  10381  fin1a2lem11  10518  fin1a2lem12  10519  hsmex  10540  axdc3lem2  10559  zorn2lem1  10604  zorn2lem6  10609  zorn2lem7  10610  zorn2g  10611  wuncval  10857  tskmval  10954  peano5uzti  12819  uzval  12997  rpnnen1  13141  ixxval  13514  fzval  13671  hashbclem  14627  hashbc  14628  shftfn  15258  bitsfval  16625  sadfval  16654  sadcom  16665  smufval  16679  smupp1  16682  smupval  16690  smumullem  16694  gcdval  16698  bezoutlem2  16745  bezoutlem4  16747  lcmval  16799  lcmfval  16828  lcmf0val  16829  lcmfpr  16834  isprm  16880  odzval  17001  pcval  17054  pceulem  17055  pceu  17056  pczpre  17057  pcdiv  17062  prmreclem1  17126  prmreclem4  17129  prmreclem5  17130  ramval  17218  cshws0  17311  imasdsval  17719  mrcval  17816  eldmcoa  18272  chneq1  18818  cycsubg2  19457  cntzval  19568  cntzsnval  19571  odfval  19779  odfvalALT  19780  odval  19781  gexval  19825  efgsfo  19986  dprdval  20252  ablfac1a  20318  ablfac1b  20319  ablfac1eu  20322  ablfaclem1  20334  ablfaclem3  20336  rnghmval  20703  rhmval0  20738  rgspnval  20897  lspval  21283  ocvval  22006  dsmmelbas  22078  frlmsslss  22113  aspval  22213  psrass1lem  22274  psrmulval  22285  mplmonmul  22378  mhpval  22493  mhpmulcl  22503  coe1mul2  22621  pmatcoe1fsupp  23052  istopon  23263  toponsspwpw  23273  clsval  23388  neival  23453  ordtbaslem  23539  ordtbas2  23542  ordtopn1  23545  ordtopn2  23546  cnpval  23587  llyeq  23822  nllyeq  23823  ptfinfin  23871  finlocfin  23872  dissnlocfin  23881  locfindis  23882  xkoopn  23941  kqfval  24075  tsmsfbas  24480  blvalps  24737  blval  24738  nmofval  25066  nmoval  25067  ishtpy  25326  minveclem3b  25782  minveclem3  25783  minveclem4  25786  minveclem5  25787  ovolval  25827  vitalilem2  25963  vitalilem3  25964  vitalilem4  25965  vitali  25967  itg2monolem1  26104  elcpn  26287  mdegmullem  26429  elqaalem1  26675  elqaalem2  26676  elqaalem3  26677  elqaa  26678  aannenlem1  26688  aannenlem2  26689  jensen  27349  vmaval  27473  muval  27492  sgmval  27502  fsumdvdscom  27545  musum  27551  muinv  27553  dchrisum0fval  27865  dchrisum0ff  27867  logsqvma2  27903  pntrlog2bndlem1  27937  cutsval  28199  bdayons  28695  tglngval  29047  plngval  29288  ttgval  29485  ttgitvval  29492  ebtwntg  29593  numedglnl  29755  dfnbgr2  29951  dfnbgr3  29952  uvtxusgr  30016  vtxdgval  30082  rusgrnumwrdl2  30200  iswwlksnon  30475  rusgrnumwwlks  30599  hashecclwwlkn1  30701  umgrhashecclwwlk  30702  clwlknf1oclwwlknlem2  30706  clwwlknon  30714  clwwlk0on0  30716  eupth2  30873  fusgreg2wsplem  30967  fusgreghash2wsp  30972  numclwlk1lem1  31003  sspval  31358  ubthlem1  31505  ubthlem2  31506  ubthlem3  31507  ocval  31915  spanval  31968  chsupid  32047  eigvecval  32531  specval  32533  fcobijfs2  33387  pwrssmgc  33637  fxpgaval  33804  nsgqusf1olem3  34050  selvply1rhmlemb  34234  mplvrpmrhm  34262  psrmonmul  34265  esplyfval  34278  esplyfval0  34279  minplyval  34420  constrsuc  34453  constrcbvlem  34470  crefeq  34560  zarcls1  34584  zarclsun  34585  zarclsiin  34586  zarclsint  34587  zarclssn  34588  zartop  34591  zartopon  34592  zart0  34594  zarmxt1  34595  zarcmp  34597  rhmpreimacnlem  34599  rhmpreimacn  34600  ordtcnvNEW  34635  ordtrest2NEW  34638  ordtconnlem1  34639  measvuni  34930  brfae  34964  omsfval  35009  orvcelval  35184  ballotlemi  35216  bnj602  35628  werankwe  35834  werankwe2  35835  rankse  35836  fineqvnttrclselem2  35903  fineqvnttrclselem3  35904  fineqvnttrclse  35905  onvf1odlem3  36046  onprcf1acwevdlem2  36059  onf1oracwevd  36065  subfacp1lem6  36130  kur14  36161  cvmscbv  36203  cvmsi  36210  cvmsval  36211  snmlval  36276  snmlflim  36277  satfv0  36303  satfv1  36308  satfv0fun  36316  satffunlem1lem1  36347  satffunlem2lem1  36349  satfv0fvfmla0  36358  satfv1fvfmla1  36368  prv1n  36376  fvray  37097  fwddifnval  37119  nmulprop  37130  nmulcom  37134  neibastop3  37341  weiunlem  37442  icoreval  38481  fin2so  38735  poimirlem26  38769  poimirlem27  38770  poimirlem28  38771  poimirlem32  38775  ftc1anclem6  38821  islinei  41000  pmapval  41017  paddval  41058  paddcom  41073  pclvalN  41150  ldilset  41369  dilsetN  41413  diafval  42291  diaval  42292  docavalN  42383  dicfval  42435  dochfval  42610  dochval  42611  mapdval  42888  mapdsn2  42902  grpods  43447  unitscyglem1  43448  unitscyglem2  43449  unitscyglem3  43450  unitscyglem4  43451  frlmnzcoordval  43857  prjcrvval  43872  2rexfrabdioph  44007  3rexfrabdioph  44008  4rexfrabdioph  44009  6rexfrabdioph  44010  7rexfrabdioph  44011  eldioph4i  44023  diophren  44024  pell1qrval  44057  pell14qrval  44059  pell1234qrval  44061  rpnnen3  44243  pwssplit4  44295  pwslnmlem2  44299  dgraaval  44349  itgoval  44366  proot1hash  44400  rp-intrabeq  44426  rp-unirabeq  44427  rfovfvd  45205  rfovfvfvd  45206  rfovcnvf1od  45207  fsovrfovd  45212  fsovfvd  45213  fsovfvfvd  45214  fsovcnvlem  45216  nzss  45504  supminfxr  46689  dvnprodlem1  47171  dvnprodlem2  47172  dvnprodlem3  47173  dvnprod  47174  stoweidlem26  47251  stoweidlem27  47252  stoweidlem31  47256  stoweidlem34  47259  stoweidlem46  47271  fourierdlem79  47410  fourierdlem96  47427  fourierdlem97  47428  fourierdlem98  47429  fourierdlem99  47430  fourierdlem105  47436  fourierdlem107  47438  fourierdlem108  47439  fourierdlem110  47441  etransclem11  47470  salgenval  47546  subsaliuncl  47583  ovnval  47766  ovnval2  47770  ovnval2b  47777  ovncvrrp  47789  ovnsubaddlem1  47795  ovnsubadd  47797  ovncvr2  47836  hspmbl  47854  ovolval2  47869  ovnovollem3  47883  salpreimagelt  47932  salpreimalegt  47934  salpreimagtge  47950  salpreimaltle  47951  issmflem  47952  issmf  47953  salpreimagtlt  47955  smfpreimalt  47956  smfpreimaltf  47961  issmfle  47970  smfpimltxr  47972  smfpreimale  47979  issmfgt  47981  smfpreimagt  47987  issmfge  47995  smflimlem3  47998  smflimlem4  47999  smflim  48002  smfpimgtxr  48005  smfpreimage  48007  tmachlem-agreeself  48161  tmachlem-agreeprod  48162  fvmptrabdm  48578  elsetpreimafveq  48694  prmdvdsfmtnof1  48887  fppr  49039  dfclnbgr2  49136  dfclnbgr3  49139  dfsclnbgr6  49171  grlimedgclnbgr  49308  grlimgrtri  49316  grilcbri2  49324  bigoval  49876  line  50060  rrxline  50062  sphere  50074  line2y  50082  inpw  50151