Theorem rabbidv 3421

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-rab 3415

This theorem is used by:  difeq2  4071  seex  5618  mptiniseg  6239  dfpred3g  6315  iunpreima  7065  elovmporab  7664  elovmpt3rab1  7678  naddcllem  8668  naddov2  8671  naddcom  8675  naddrid  8676  naddass  8689  fineqvlem  9240  mapfien2  9383  supeq1  9419  supeq2  9422  supeq3  9423  oieq1  9488  oieq2  9489  ordtypecbv  9493  ordtypelem3  9496  harval  9536  inf3lema  9607  wemapwe  9680  oef1o  9681  tz9.12lem3  9775  rankvalb  9783  rankvalg  9803  ranksnb  9813  rankonidlem  9814  cardval3  9961  cardidm  9968  alephsuc2  10087  coftr  10279  fin1a2lem11  10416  fin1a2lem12  10417  hsmex  10438  axdc3lem2  10457  zorn2lem1  10502  zorn2lem6  10507  zorn2lem7  10508  zorn2g  10509  wuncval  10755  tskmval  10852  peano5uzti  12715  uzval  12893  rpnnen1  13037  ixxval  13410  fzval  13567  hashbclem  14521  hashbc  14522  shftfn  15150  bitsfval  16519  sadfval  16548  sadcom  16559  smufval  16573  smupp1  16576  smupval  16584  smumullem  16588  gcdval  16592  bezoutlem2  16636  bezoutlem4  16638  lcmval  16688  lcmfval  16717  lcmf0val  16718  lcmfpr  16723  isprm  16769  odzval  16889  pcval  16942  pceulem  16943  pceu  16944  pczpre  16945  pcdiv  16950  prmreclem1  17014  prmreclem4  17017  prmreclem5  17018  ramval  17106  cshws0  17199  imasdsval  17607  mrcval  17704  eldmcoa  18160  chneq1  18706  cycsubg2  19344  cntzval  19454  cntzsnval  19457  odfval  19665  odfvalALT  19666  odval  19667  gexval  19711  efgsfo  19872  dprdval  20138  ablfac1a  20204  ablfac1b  20205  ablfac1eu  20208  ablfaclem1  20220  ablfaclem3  20222  rnghmval  20587  rhmval0  20622  rgspnval  20780  lspval  21165  ocvval  21886  dsmmelbas  21958  frlmsslss  21993  aspval  22093  psrass1lem  22154  psrmulval  22165  mplmonmul  22258  mhpval  22373  mhpmulcl  22383  coe1mul2  22501  pmatcoe1fsupp  22932  istopon  23143  toponsspwpw  23153  clsval  23268  neival  23333  ordtbaslem  23419  ordtbas2  23422  ordtopn1  23425  ordtopn2  23426  cnpval  23467  llyeq  23702  nllyeq  23703  ptfinfin  23751  finlocfin  23752  dissnlocfin  23761  locfindis  23762  xkoopn  23821  kqfval  23955  tsmsfbas  24360  blvalps  24617  blval  24618  nmofval  24946  nmoval  24947  ishtpy  25206  minveclem3b  25662  minveclem3  25663  minveclem4  25666  minveclem5  25667  ovolval  25707  vitalilem2  25843  vitalilem3  25844  vitalilem4  25845  vitali  25847  itg2monolem1  25984  elcpn  26168  mdegmullem  26310  elqaalem1  26558  elqaalem2  26559  elqaalem3  26560  elqaa  26561  aannenlem1  26571  aannenlem2  26572  jensen  27233  vmaval  27357  muval  27376  sgmval  27386  fsumdvdscom  27429  musum  27435  muinv  27437  dchrisum0fval  27749  dchrisum0ff  27751  logsqvma2  27787  pntrlog2bndlem1  27821  cutsval  28053  bdayons  28549  tglngval  28901  plngval  29142  ttgval  29339  ttgitvval  29346  ebtwntg  29447  numedglnl  29609  dfnbgr2  29805  dfnbgr3  29806  uvtxusgr  29870  vtxdgval  29936  rusgrnumwrdl2  30054  iswwlksnon  30329  rusgrnumwwlks  30453  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  clwlknf1oclwwlknlem2  30560  clwwlknon  30568  clwwlk0on0  30570  eupth2  30727  fusgreg2wsplem  30821  fusgreghash2wsp  30826  numclwlk1lem1  30857  sspval  31212  ubthlem1  31359  ubthlem2  31360  ubthlem3  31361  ocval  31769  spanval  31822  chsupid  31901  eigvecval  32385  specval  32387  fcobijfs2  33201  pwrssmgc  33448  fxpgaval  33615  nsgqusf1olem3  33852  selvply1rhmlemb  34037  mplvrpmrhm  34065  psrmonmul  34068  esplyfval  34081  esplyfval0  34082  minplyval  34223  constrsuc  34256  constrcbvlem  34273  crefeq  34363  zarcls1  34387  zarclsun  34388  zarclsiin  34389  zarclsint  34390  zarclssn  34391  zartop  34394  zartopon  34395  zart0  34397  zarmxt1  34398  zarcmp  34400  rhmpreimacnlem  34402  rhmpreimacn  34403  ordtcnvNEW  34438  ordtrest2NEW  34441  ordtconnlem1  34442  measvuni  34733  brfae  34767  omsfval  34813  orvcelval  34988  ballotlemi  35020  bnj602  35432  fineqvnttrclselem2  35656  fineqvnttrclselem3  35657  fineqvnttrclse  35658  onvf1odlem3  35710  subfacp1lem6  35772  kur14  35803  cvmscbv  35845  cvmsi  35852  cvmsval  35853  snmlval  35918  snmlflim  35919  satfv0  35945  satfv1  35950  satfv0fun  35958  satffunlem1lem1  35989  satffunlem2lem1  35991  satfv0fvfmla0  36000  satfv1fvfmla1  36010  prv1n  36018  fvray  36729  fwddifnval  36751  nmulprop  36778  nmulcom  36782  neibastop3  36989  weiunlem  37090  icoreval  38115  fin2so  38369  poimirlem26  38403  poimirlem27  38404  poimirlem28  38405  poimirlem32  38409  ftc1anclem6  38455  islinei  40621  pmapval  40638  paddval  40679  paddcom  40694  pclvalN  40771  ldilset  40990  dilsetN  41034  diafval  41912  diaval  41913  docavalN  42004  dicfval  42056  dochfval  42231  dochval  42232  mapdval  42509  mapdsn2  42523  grpods  43068  unitscyglem1  43069  unitscyglem2  43070  unitscyglem3  43071  unitscyglem4  43072  prjcrvval  43486  2rexfrabdioph  43645  3rexfrabdioph  43646  4rexfrabdioph  43647  6rexfrabdioph  43648  7rexfrabdioph  43649  eldioph4i  43661  diophren  43662  pell1qrval  43695  pell14qrval  43697  pell1234qrval  43699  rpnnen3  43881  fnwe2lem1  43899  pwssplit4  43938  pwslnmlem2  43942  dgraaval  43993  itgoval  44010  proot1hash  44044  rp-intrabeq  44070  rp-unirabeq  44071  rfovfvd  44850  rfovfvfvd  44851  rfovcnvf1od  44852  fsovrfovd  44857  fsovfvd  44858  fsovfvfvd  44859  fsovcnvlem  44861  nzss  45149  supminfxr  46300  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  dvnprod  46785  stoweidlem26  46862  stoweidlem27  46863  stoweidlem31  46867  stoweidlem34  46870  stoweidlem46  46882  fourierdlem79  47021  fourierdlem96  47038  fourierdlem97  47039  fourierdlem98  47040  fourierdlem99  47041  fourierdlem105  47047  fourierdlem107  47049  fourierdlem108  47050  fourierdlem110  47052  etransclem11  47081  salgenval  47157  subsaliuncl  47194  ovnval  47377  ovnval2  47381  ovnval2b  47388  ovncvrrp  47400  ovnsubaddlem1  47406  ovnsubadd  47408  ovncvr2  47447  hspmbl  47465  ovolval2  47480  ovnovollem3  47494  salpreimagelt  47543  salpreimalegt  47545  salpreimagtge  47561  salpreimaltle  47562  issmflem  47563  issmf  47564  salpreimagtlt  47566  smfpreimalt  47567  smfpreimaltf  47572  issmfle  47581  smfpimltxr  47583  smfpreimale  47590  issmfgt  47592  smfpreimagt  47598  issmfge  47606  smflimlem3  47609  smflimlem4  47610  smflim  47613  smfpimgtxr  47616  smfpreimage  47618  tmachlem-agreeself  47772  tmachlem-agreeprod  47773  fvmptrabdm  48189  elsetpreimafveq  48305  prmdvdsfmtnof1  48498  fppr  48650  dfclnbgr2  48747  dfclnbgr3  48750  dfsclnbgr6  48782  grlimedgclnbgr  48919  grlimgrtri  48927  grilcbri2  48935  bigoval  49487  line  49670  rrxline  49672  sphere  49685  line2y  49693  inpw  49761