Theorem rabbidv 3390

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2110  {crab 3065

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 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-rab 3070

This theorem is referenced by:  rabeqbidv  3396  difeq2  4031  seex  5513  mptiniseg  6102  dfpred3g  6171  elovmporab  7451  elovmpt3rab1  7465  fineqvlem  8892  mapfien2  9025  supeq1  9061  supeq2  9064  supeq3  9065  oieq1  9128  oieq2  9129  ordtypecbv  9133  ordtypelem3  9136  harval  9176  inf3lema  9239  wemapwe  9312  oef1o  9313  tz9.12lem3  9405  rankvalb  9413  rankvalg  9433  ranksnb  9443  rankonidlem  9444  cardval3  9568  cardidm  9575  alephsuc2  9694  coftr  9887  fin1a2lem11  10024  fin1a2lem12  10025  hsmex  10046  axdc3lem2  10065  zorn2lem1  10110  zorn2lem6  10115  zorn2lem7  10116  zorn2g  10117  wuncval  10356  tskmval  10453  peano5uzti  12267  uzval  12440  rpnnen1  12579  ixxval  12943  fzval  13097  hashbclem  14016  hashbc  14017  shftfn  14636  bitsfval  15982  sadfval  16011  sadcom  16022  smufval  16036  smupp1  16039  smupval  16047  smumullem  16051  gcdval  16055  bezoutlem2  16100  bezoutlem4  16102  lcmval  16149  lcmfval  16178  lcmf0val  16179  lcmfpr  16184  isprm  16230  odzval  16344  pcval  16397  pceulem  16398  pceu  16399  pczpre  16400  pcdiv  16405  prmreclem1  16469  prmreclem4  16472  prmreclem5  16473  ramval  16561  cshws0  16655  imasdsval  17020  mrcval  17113  eldmcoa  17571  cycsubg2  18617  cntzval  18715  cntzsnval  18718  odfval  18924  odfvalALT  18925  odval  18926  gexval  18967  efgsfo  19129  dprdval  19390  ablfac1a  19456  ablfac1b  19457  ablfac1eu  19460  ablfaclem1  19472  ablfaclem3  19474  lspval  20012  ocvval  20629  dsmmelbas  20701  frlmsslss  20736  aspval  20832  psrass1lemOLD  20899  psrass1lem  20902  psrmulval  20911  mplmonmul  20993  mhpval  21080  mhpmulcl  21089  coe1mul2  21190  pmatcoe1fsupp  21598  istopon  21809  toponsspwpw  21819  clsval  21934  neival  21999  ordtbaslem  22085  ordtbas2  22088  ordtopn1  22091  ordtopn2  22092  cnpval  22133  llyeq  22367  nllyeq  22368  ptfinfin  22416  finlocfin  22417  dissnlocfin  22426  locfindis  22427  xkoopn  22486  kqfval  22620  tsmsfbas  23025  blvalps  23283  blval  23284  nmofval  23612  nmoval  23613  ishtpy  23869  minveclem3b  24325  minveclem3  24326  minveclem4  24329  minveclem5  24330  ovolval  24370  vitalilem2  24506  vitalilem3  24507  vitalilem4  24508  vitali  24510  itg2monolem1  24648  elcpn  24831  mdegmullem  24976  elqaalem1  25212  elqaalem2  25213  elqaalem3  25214  elqaa  25215  aannenlem1  25221  aannenlem2  25222  jensen  25871  vmaval  25995  muval  26014  sgmval  26024  fsumdvdscom  26067  musum  26073  muinv  26075  dchrisum0fval  26386  dchrisum0ff  26388  logsqvma2  26424  pntrlog2bndlem1  26458  tglngval  26642  ttgval  26966  ttgitvval  26973  ebtwntg  27073  numedglnl  27235  dfnbgr2  27425  dfnbgr3  27426  uvtxusgr  27490  vtxdgval  27556  rusgrnumwrdl2  27674  iswwlksnon  27937  rusgrnumwwlks  28058  hashecclwwlkn1  28160  umgrhashecclwwlk  28161  clwlknf1oclwwlknlem2  28165  clwwlknon  28173  clwwlk0on0  28175  eupth2  28322  fusgreg2wsplem  28416  fusgreghash2wsp  28421  numclwlk1lem1  28452  sspval  28804  ubthlem1  28951  ubthlem2  28952  ubthlem3  28953  ocval  29361  spanval  29414  chsupid  29493  eigvecval  29977  specval  29979  iunpreima  30623  pwrssmgc  30997  nsgqusf1olem3  31314  crefeq  31509  zarcls1  31533  zarclsun  31534  zarclsiin  31535  zarclsint  31536  zarclssn  31537  zartop  31540  zartopon  31541  zart0  31543  zarmxt1  31544  zarcmp  31546  rhmpreimacnlem  31548  rhmpreimacn  31549  ordtcnvNEW  31584  ordtrest2NEW  31587  ordtconnlem1  31588  measvuni  31894  brfae  31928  omsfval  31973  orvcelval  32147  ballotlemi  32179  bnj602  32608  subfacp1lem6  32860  kur14  32891  cvmscbv  32933  cvmsi  32940  cvmsval  32941  snmlval  33006  snmlflim  33007  satfv0  33033  satfv1  33038  satfv0fun  33046  satffunlem1lem1  33077  satffunlem2lem1  33079  satfv0fvfmla0  33088  satfv1fvfmla1  33098  prv1n  33106  naddcllem  33568  naddov2  33571  naddcom  33572  naddid1  33573  scutval  33731  fvray  34180  fwddifnval  34202  neibastop3  34288  icoreval  35261  fin2so  35501  poimirlem26  35540  poimirlem27  35541  poimirlem28  35542  poimirlem32  35546  ftc1anclem6  35592  islinei  37491  pmapval  37508  paddval  37549  paddcom  37564  pclvalN  37641  ldilset  37860  dilsetN  37904  diafval  38782  diaval  38783  docavalN  38874  dicfval  38926  dochfval  39101  dochval  39102  mapdval  39379  mapdsn2  39393  2rexfrabdioph  40321  3rexfrabdioph  40322  4rexfrabdioph  40323  6rexfrabdioph  40324  7rexfrabdioph  40325  eldioph4i  40337  diophren  40338  pell1qrval  40371  pell14qrval  40373  pell1234qrval  40375  rpnnen3  40557  fnwe2lem1  40578  pwssplit4  40617  pwslnmlem2  40621  dgraaval  40672  itgoval  40689  rgspnval  40696  proot1hash  40728  rfovfvd  41287  rfovfvfvd  41288  rfovcnvf1od  41289  fsovrfovd  41294  fsovfvd  41295  fsovfvfvd  41296  fsovcnvlem  41298  nzss  41608  supminfxr  42679  dvnprodlem1  43162  dvnprodlem2  43163  dvnprodlem3  43164  dvnprod  43165  stoweidlem26  43242  stoweidlem27  43243  stoweidlem31  43247  stoweidlem34  43250  stoweidlem46  43262  fourierdlem79  43401  fourierdlem96  43418  fourierdlem97  43419  fourierdlem98  43420  fourierdlem99  43421  fourierdlem105  43427  fourierdlem107  43429  fourierdlem108  43430  fourierdlem110  43432  etransclem11  43461  salgenval  43537  subsaliuncl  43572  ovnval  43754  ovnval2  43758  ovnval2b  43765  ovncvrrp  43777  ovnsubaddlem1  43783  ovnsubadd  43785  ovncvr2  43824  hspmbl  43842  ovolval2  43857  ovnovollem3  43871  salpreimagelt  43917  salpreimalegt  43919  salpreimagtge  43933  salpreimaltle  43934  issmflem  43935  issmf  43936  salpreimagtlt  43938  smfpreimalt  43939  smfpreimaltf  43944  issmfle  43953  smfpimltxr  43955  smfpreimale  43962  issmfgt  43964  smfpreimagt  43969  issmfge  43977  smflimlem3  43980  smflimlem4  43981  smflim  43984  smfpimgtxr  43987  smfpreimage  43989  fvmptrabdm  44457  elsetpreimafveq  44522  prmdvdsfmtnof1  44712  fppr  44851  rnghmval  45122  bigoval  45568  line  45751  rrxline  45753  sphere  45766  line2y  45774  inpw  45837