Theorem rabbidv 3411

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ∈ wcel 2105  {crab 3403

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-rab 3404

This theorem is referenced by:  difeq2  4064  seex  5583  mptiniseg  6178  dfpred3g  6251  elovmporab  7578  elovmpt3rab1  7592  fineqvlem  9128  mapfien2  9267  supeq1  9303  supeq2  9306  supeq3  9307  oieq1  9370  oieq2  9371  ordtypecbv  9375  ordtypelem3  9378  harval  9418  inf3lema  9482  wemapwe  9555  oef1o  9556  tz9.12lem3  9647  rankvalb  9655  rankvalg  9675  ranksnb  9685  rankonidlem  9686  cardval3  9810  cardidm  9817  alephsuc2  9938  coftr  10131  fin1a2lem11  10268  fin1a2lem12  10269  hsmex  10290  axdc3lem2  10309  zorn2lem1  10354  zorn2lem6  10359  zorn2lem7  10360  zorn2g  10361  wuncval  10600  tskmval  10697  peano5uzti  12512  uzval  12686  rpnnen1  12825  ixxval  13189  fzval  13343  hashbclem  14265  hashbc  14266  shftfn  14884  bitsfval  16230  sadfval  16259  sadcom  16270  smufval  16284  smupp1  16287  smupval  16295  smumullem  16299  gcdval  16303  bezoutlem2  16348  bezoutlem4  16350  lcmval  16395  lcmfval  16424  lcmf0val  16425  lcmfpr  16430  isprm  16476  odzval  16590  pcval  16643  pceulem  16644  pceu  16645  pczpre  16646  pcdiv  16651  prmreclem1  16715  prmreclem4  16718  prmreclem5  16719  ramval  16807  cshws0  16901  imasdsval  17324  mrcval  17417  eldmcoa  17878  cycsubg2  18926  cntzval  19024  cntzsnval  19027  odfval  19237  odfvalALT  19238  odval  19239  gexval  19280  efgsfo  19441  dprdval  19702  ablfac1a  19768  ablfac1b  19769  ablfac1eu  19772  ablfaclem1  19784  ablfaclem3  19786  lspval  20344  ocvval  20979  dsmmelbas  21053  frlmsslss  21088  aspval  21184  psrass1lemOLD  21250  psrass1lem  21253  psrmulval  21262  mplmonmul  21344  mhpval  21437  mhpmulcl  21446  coe1mul2  21547  pmatcoe1fsupp  21957  istopon  22168  toponsspwpw  22178  clsval  22295  neival  22360  ordtbaslem  22446  ordtbas2  22449  ordtopn1  22452  ordtopn2  22453  cnpval  22494  llyeq  22728  nllyeq  22729  ptfinfin  22777  finlocfin  22778  dissnlocfin  22787  locfindis  22788  xkoopn  22847  kqfval  22981  tsmsfbas  23386  blvalps  23645  blval  23646  nmofval  23985  nmoval  23986  ishtpy  24242  minveclem3b  24699  minveclem3  24700  minveclem4  24703  minveclem5  24704  ovolval  24744  vitalilem2  24880  vitalilem3  24881  vitalilem4  24882  vitali  24884  itg2monolem1  25022  elcpn  25205  mdegmullem  25350  elqaalem1  25586  elqaalem2  25587  elqaalem3  25588  elqaa  25589  aannenlem1  25595  aannenlem2  25596  jensen  26245  vmaval  26369  muval  26388  sgmval  26398  fsumdvdscom  26441  musum  26447  muinv  26449  dchrisum0fval  26760  dchrisum0ff  26762  logsqvma2  26798  pntrlog2bndlem1  26832  scutval  27046  tglngval  27202  ttgval  27526  ttgvalOLD  27527  ttgitvval  27539  ebtwntg  27640  numedglnl  27804  dfnbgr2  27994  dfnbgr3  27995  uvtxusgr  28059  vtxdgval  28125  rusgrnumwrdl2  28243  iswwlksnon  28507  rusgrnumwwlks  28628  hashecclwwlkn1  28730  umgrhashecclwwlk  28731  clwlknf1oclwwlknlem2  28735  clwwlknon  28743  clwwlk0on0  28745  eupth2  28892  fusgreg2wsplem  28986  fusgreghash2wsp  28991  numclwlk1lem1  29022  sspval  29374  ubthlem1  29521  ubthlem2  29522  ubthlem3  29523  ocval  29931  spanval  29984  chsupid  30063  eigvecval  30547  specval  30549  iunpreima  31191  pwrssmgc  31565  nsgqusf1olem3  31897  crefeq  32093  zarcls1  32117  zarclsun  32118  zarclsiin  32119  zarclsint  32120  zarclssn  32121  zartop  32124  zartopon  32125  zart0  32127  zarmxt1  32128  zarcmp  32130  rhmpreimacnlem  32132  rhmpreimacn  32133  ordtcnvNEW  32168  ordtrest2NEW  32171  ordtconnlem1  32172  measvuni  32480  brfae  32514  omsfval  32561  orvcelval  32735  ballotlemi  32767  bnj602  33194  subfacp1lem6  33446  kur14  33477  cvmscbv  33519  cvmsi  33526  cvmsval  33527  snmlval  33592  snmlflim  33593  satfv0  33619  satfv1  33624  satfv0fun  33632  satffunlem1lem1  33663  satffunlem2lem1  33665  satfv0fvfmla0  33674  satfv1fvfmla1  33684  prv1n  33692  naddcllem  34116  naddov2  34119  naddcom  34122  naddid1  34123  naddass  34134  fvray  34582  fwddifnval  34604  neibastop3  34690  icoreval  35680  fin2so  35920  poimirlem26  35959  poimirlem27  35960  poimirlem28  35961  poimirlem32  35965  ftc1anclem6  36011  islinei  38059  pmapval  38076  paddval  38117  paddcom  38132  pclvalN  38209  ldilset  38428  dilsetN  38472  diafval  39350  diaval  39351  docavalN  39442  dicfval  39494  dochfval  39669  dochval  39670  mapdval  39947  mapdsn2  39961  prjcrvval  40782  2rexfrabdioph  40931  3rexfrabdioph  40932  4rexfrabdioph  40933  6rexfrabdioph  40934  7rexfrabdioph  40935  eldioph4i  40947  diophren  40948  pell1qrval  40981  pell14qrval  40983  pell1234qrval  40985  rpnnen3  41168  fnwe2lem1  41189  pwssplit4  41228  pwslnmlem2  41232  dgraaval  41283  itgoval  41300  rgspnval  41307  proot1hash  41339  rfovfvd  41983  rfovfvfvd  41984  rfovcnvf1od  41985  fsovrfovd  41990  fsovfvd  41991  fsovfvfvd  41992  fsovcnvlem  41994  nzss  42308  supminfxr  43391  dvnprodlem1  43875  dvnprodlem2  43876  dvnprodlem3  43877  dvnprod  43878  stoweidlem26  43955  stoweidlem27  43956  stoweidlem31  43960  stoweidlem34  43963  stoweidlem46  43975  fourierdlem79  44114  fourierdlem96  44131  fourierdlem97  44132  fourierdlem98  44133  fourierdlem99  44134  fourierdlem105  44140  fourierdlem107  44142  fourierdlem108  44143  fourierdlem110  44145  etransclem11  44174  salgenval  44250  subsaliuncl  44285  ovnval  44468  ovnval2  44472  ovnval2b  44479  ovncvrrp  44491  ovnsubaddlem1  44497  ovnsubadd  44499  ovncvr2  44538  hspmbl  44556  ovolval2  44571  ovnovollem3  44585  salpreimagelt  44634  salpreimalegt  44636  salpreimagtge  44652  salpreimaltle  44653  issmflem  44654  issmf  44655  salpreimagtlt  44657  smfpreimalt  44658  smfpreimaltf  44663  issmfle  44672  smfpimltxr  44674  smfpreimale  44681  issmfgt  44683  smfpreimagt  44689  issmfge  44697  smflimlem3  44700  smflimlem4  44701  smflim  44704  smfpimgtxr  44707  smfpreimage  44709  fvmptrabdm  45203  elsetpreimafveq  45267  prmdvdsfmtnof1  45457  fppr  45596  rnghmval  45867  bigoval  46313  line  46496  rrxline  46498  sphere  46511  line2y  46519  inpw  46582