Theorem rabbidv 3404

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2108  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3072

This theorem is referenced by:  rabeqbidv  3410  difeq2  4047  seex  5542  mptiniseg  6131  dfpred3g  6203  elovmporab  7493  elovmpt3rab1  7507  fineqvlem  8966  mapfien2  9098  supeq1  9134  supeq2  9137  supeq3  9138  oieq1  9201  oieq2  9202  ordtypecbv  9206  ordtypelem3  9209  harval  9249  inf3lema  9312  wemapwe  9385  oef1o  9386  tz9.12lem3  9478  rankvalb  9486  rankvalg  9506  ranksnb  9516  rankonidlem  9517  cardval3  9641  cardidm  9648  alephsuc2  9767  coftr  9960  fin1a2lem11  10097  fin1a2lem12  10098  hsmex  10119  axdc3lem2  10138  zorn2lem1  10183  zorn2lem6  10188  zorn2lem7  10189  zorn2g  10190  wuncval  10429  tskmval  10526  peano5uzti  12340  uzval  12513  rpnnen1  12652  ixxval  13016  fzval  13170  hashbclem  14092  hashbc  14093  shftfn  14712  bitsfval  16058  sadfval  16087  sadcom  16098  smufval  16112  smupp1  16115  smupval  16123  smumullem  16127  gcdval  16131  bezoutlem2  16176  bezoutlem4  16178  lcmval  16225  lcmfval  16254  lcmf0val  16255  lcmfpr  16260  isprm  16306  odzval  16420  pcval  16473  pceulem  16474  pceu  16475  pczpre  16476  pcdiv  16481  prmreclem1  16545  prmreclem4  16548  prmreclem5  16549  ramval  16637  cshws0  16731  imasdsval  17143  mrcval  17236  eldmcoa  17696  cycsubg2  18744  cntzval  18842  cntzsnval  18845  odfval  19055  odfvalALT  19056  odval  19057  gexval  19098  efgsfo  19260  dprdval  19521  ablfac1a  19587  ablfac1b  19588  ablfac1eu  19591  ablfaclem1  19603  ablfaclem3  19605  lspval  20152  ocvval  20784  dsmmelbas  20856  frlmsslss  20891  aspval  20987  psrass1lemOLD  21053  psrass1lem  21056  psrmulval  21065  mplmonmul  21147  mhpval  21240  mhpmulcl  21249  coe1mul2  21350  pmatcoe1fsupp  21758  istopon  21969  toponsspwpw  21979  clsval  22096  neival  22161  ordtbaslem  22247  ordtbas2  22250  ordtopn1  22253  ordtopn2  22254  cnpval  22295  llyeq  22529  nllyeq  22530  ptfinfin  22578  finlocfin  22579  dissnlocfin  22588  locfindis  22589  xkoopn  22648  kqfval  22782  tsmsfbas  23187  blvalps  23446  blval  23447  nmofval  23784  nmoval  23785  ishtpy  24041  minveclem3b  24497  minveclem3  24498  minveclem4  24501  minveclem5  24502  ovolval  24542  vitalilem2  24678  vitalilem3  24679  vitalilem4  24680  vitali  24682  itg2monolem1  24820  elcpn  25003  mdegmullem  25148  elqaalem1  25384  elqaalem2  25385  elqaalem3  25386  elqaa  25387  aannenlem1  25393  aannenlem2  25394  jensen  26043  vmaval  26167  muval  26186  sgmval  26196  fsumdvdscom  26239  musum  26245  muinv  26247  dchrisum0fval  26558  dchrisum0ff  26560  logsqvma2  26596  pntrlog2bndlem1  26630  tglngval  26816  ttgval  27140  ttgitvval  27152  ebtwntg  27253  numedglnl  27417  dfnbgr2  27607  dfnbgr3  27608  uvtxusgr  27672  vtxdgval  27738  rusgrnumwrdl2  27856  iswwlksnon  28119  rusgrnumwwlks  28240  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwlknf1oclwwlknlem2  28347  clwwlknon  28355  clwwlk0on0  28357  eupth2  28504  fusgreg2wsplem  28598  fusgreghash2wsp  28603  numclwlk1lem1  28634  sspval  28986  ubthlem1  29133  ubthlem2  29134  ubthlem3  29135  ocval  29543  spanval  29596  chsupid  29675  eigvecval  30159  specval  30161  iunpreima  30805  pwrssmgc  31180  nsgqusf1olem3  31502  crefeq  31697  zarcls1  31721  zarclsun  31722  zarclsiin  31723  zarclsint  31724  zarclssn  31725  zartop  31728  zartopon  31729  zart0  31731  zarmxt1  31732  zarcmp  31734  rhmpreimacnlem  31736  rhmpreimacn  31737  ordtcnvNEW  31772  ordtrest2NEW  31775  ordtconnlem1  31776  measvuni  32082  brfae  32116  omsfval  32161  orvcelval  32335  ballotlemi  32367  bnj602  32795  subfacp1lem6  33047  kur14  33078  cvmscbv  33120  cvmsi  33127  cvmsval  33128  snmlval  33193  snmlflim  33194  satfv0  33220  satfv1  33225  satfv0fun  33233  satffunlem1lem1  33264  satffunlem2lem1  33266  satfv0fvfmla0  33275  satfv1fvfmla1  33285  prv1n  33293  naddcllem  33758  naddov2  33761  naddcom  33762  naddid1  33763  scutval  33921  fvray  34370  fwddifnval  34392  neibastop3  34478  icoreval  35451  fin2so  35691  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem32  35736  ftc1anclem6  35782  islinei  37681  pmapval  37698  paddval  37739  paddcom  37754  pclvalN  37831  ldilset  38050  dilsetN  38094  diafval  38972  diaval  38973  docavalN  39064  dicfval  39116  dochfval  39291  dochval  39292  mapdval  39569  mapdsn2  39583  2rexfrabdioph  40534  3rexfrabdioph  40535  4rexfrabdioph  40536  6rexfrabdioph  40537  7rexfrabdioph  40538  eldioph4i  40550  diophren  40551  pell1qrval  40584  pell14qrval  40586  pell1234qrval  40588  rpnnen3  40770  fnwe2lem1  40791  pwssplit4  40830  pwslnmlem2  40834  dgraaval  40885  itgoval  40902  rgspnval  40909  proot1hash  40941  rfovfvd  41499  rfovfvfvd  41500  rfovcnvf1od  41501  fsovrfovd  41506  fsovfvd  41507  fsovfvfvd  41508  fsovcnvlem  41510  nzss  41824  supminfxr  42894  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  dvnprod  43380  stoweidlem26  43457  stoweidlem27  43458  stoweidlem31  43462  stoweidlem34  43465  stoweidlem46  43477  fourierdlem79  43616  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem105  43642  fourierdlem107  43644  fourierdlem108  43645  fourierdlem110  43647  etransclem11  43676  salgenval  43752  subsaliuncl  43787  ovnval  43969  ovnval2  43973  ovnval2b  43980  ovncvrrp  43992  ovnsubaddlem1  43998  ovnsubadd  44000  ovncvr2  44039  hspmbl  44057  ovolval2  44072  ovnovollem3  44086  salpreimagelt  44132  salpreimalegt  44134  salpreimagtge  44148  salpreimaltle  44149  issmflem  44150  issmf  44151  salpreimagtlt  44153  smfpreimalt  44154  smfpreimaltf  44159  issmfle  44168  smfpimltxr  44170  smfpreimale  44177  issmfgt  44179  smfpreimagt  44184  issmfge  44192  smflimlem3  44195  smflimlem4  44196  smflim  44199  smfpimgtxr  44202  smfpreimage  44204  fvmptrabdm  44672  elsetpreimafveq  44737  prmdvdsfmtnof1  44927  fppr  45066  rnghmval  45337  bigoval  45783  line  45966  rrxline  45968  sphere  45981  line2y  45989  inpw  46052