Theorem rabbidv 3426

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ∈ wcel 2098  {crab 3418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-rab 3419

This theorem is referenced by:  difeq2  4112  seex  5640  mptiniseg  6245  dfpred3g  6319  elovmporab  7667  elovmpt3rab1  7681  naddcllem  8697  naddov2  8700  naddcom  8703  naddrid  8704  naddass  8717  fineqvlem  9290  mapfien2  9439  supeq1  9475  supeq2  9478  supeq3  9479  oieq1  9542  oieq2  9543  ordtypecbv  9547  ordtypelem3  9550  harval  9590  inf3lema  9654  wemapwe  9727  oef1o  9728  tz9.12lem3  9819  rankvalb  9827  rankvalg  9847  ranksnb  9857  rankonidlem  9858  cardval3  9982  cardidm  9989  alephsuc2  10110  coftr  10303  fin1a2lem11  10440  fin1a2lem12  10441  hsmex  10462  axdc3lem2  10481  zorn2lem1  10526  zorn2lem6  10531  zorn2lem7  10532  zorn2g  10533  wuncval  10772  tskmval  10869  peano5uzti  12690  uzval  12862  rpnnen1  13005  ixxval  13372  fzval  13526  hashbclem  14455  hashbc  14456  shftfn  15064  bitsfval  16409  sadfval  16438  sadcom  16449  smufval  16463  smupp1  16466  smupval  16474  smumullem  16478  gcdval  16482  bezoutlem2  16527  bezoutlem4  16529  lcmval  16579  lcmfval  16608  lcmf0val  16609  lcmfpr  16614  isprm  16660  odzval  16779  pcval  16832  pceulem  16833  pceu  16834  pczpre  16835  pcdiv  16840  prmreclem1  16904  prmreclem4  16907  prmreclem5  16908  ramval  16996  cshws0  17090  imasdsval  17516  mrcval  17609  eldmcoa  18073  cycsubg2  19190  cntzval  19301  cntzsnval  19304  odfval  19516  odfvalALT  19517  odval  19518  gexval  19562  efgsfo  19723  dprdval  19989  ablfac1a  20055  ablfac1b  20056  ablfac1eu  20059  ablfaclem1  20071  ablfaclem3  20073  rnghmval  20408  lspval  20888  ocvval  21633  dsmmelbas  21707  frlmsslss  21742  aspval  21840  psrass1lemOLD  21908  psrass1lem  21911  psrmulval  21923  mplmonmul  22013  mhpval  22104  mhpmulcl  22113  coe1mul2  22230  pmatcoe1fsupp  22664  istopon  22875  toponsspwpw  22885  clsval  23002  neival  23067  ordtbaslem  23153  ordtbas2  23156  ordtopn1  23159  ordtopn2  23160  cnpval  23201  llyeq  23435  nllyeq  23436  ptfinfin  23484  finlocfin  23485  dissnlocfin  23494  locfindis  23495  xkoopn  23554  kqfval  23688  tsmsfbas  24093  blvalps  24352  blval  24353  nmofval  24692  nmoval  24693  ishtpy  24959  minveclem3b  25417  minveclem3  25418  minveclem4  25421  minveclem5  25422  ovolval  25463  vitalilem2  25599  vitalilem3  25600  vitalilem4  25601  vitali  25603  itg2monolem1  25741  elcpn  25925  mdegmullem  26075  elqaalem1  26316  elqaalem2  26317  elqaalem3  26318  elqaa  26319  aannenlem1  26325  aannenlem2  26326  jensen  26986  vmaval  27110  muval  27129  sgmval  27139  fsumdvdscom  27182  musum  27188  muinv  27190  dchrisum0fval  27503  dchrisum0ff  27505  logsqvma2  27541  pntrlog2bndlem1  27575  scutval  27799  tglngval  28447  ttgval  28771  ttgvalOLD  28772  ttgitvval  28784  ebtwntg  28885  numedglnl  29049  dfnbgr2  29242  dfnbgr3  29243  uvtxusgr  29307  vtxdgval  29374  rusgrnumwrdl2  29492  iswwlksnon  29756  rusgrnumwwlks  29877  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwlknf1oclwwlknlem2  29984  clwwlknon  29992  clwwlk0on0  29994  eupth2  30141  fusgreg2wsplem  30235  fusgreghash2wsp  30240  numclwlk1lem1  30271  sspval  30625  ubthlem1  30772  ubthlem2  30773  ubthlem3  30774  ocval  31182  spanval  31235  chsupid  31314  eigvecval  31798  specval  31800  iunpreima  32454  pwrssmgc  32837  nsgqusf1olem3  33248  minplyval  33526  crefeq  33597  zarcls1  33621  zarclsun  33622  zarclsiin  33623  zarclsint  33624  zarclssn  33625  zartop  33628  zartopon  33629  zart0  33631  zarmxt1  33632  zarcmp  33634  rhmpreimacnlem  33636  rhmpreimacn  33637  ordtcnvNEW  33672  ordtrest2NEW  33675  ordtconnlem1  33676  measvuni  33984  brfae  34018  omsfval  34065  orvcelval  34239  ballotlemi  34271  bnj602  34697  subfacp1lem6  34946  kur14  34977  cvmscbv  35019  cvmsi  35026  cvmsval  35027  snmlval  35092  snmlflim  35093  satfv0  35119  satfv1  35124  satfv0fun  35132  satffunlem1lem1  35163  satffunlem2lem1  35165  satfv0fvfmla0  35174  satfv1fvfmla1  35184  prv1n  35192  fvray  35888  fwddifnval  35910  neibastop3  35997  icoreval  36983  fin2so  37231  poimirlem26  37270  poimirlem27  37271  poimirlem28  37272  poimirlem32  37276  ftc1anclem6  37322  islinei  39363  pmapval  39380  paddval  39421  paddcom  39436  pclvalN  39513  ldilset  39732  dilsetN  39776  diafval  40654  diaval  40655  docavalN  40746  dicfval  40798  dochfval  40973  dochval  40974  mapdval  41251  mapdsn2  41265  prjcrvval  42196  2rexfrabdioph  42363  3rexfrabdioph  42364  4rexfrabdioph  42365  6rexfrabdioph  42366  7rexfrabdioph  42367  eldioph4i  42379  diophren  42380  pell1qrval  42413  pell14qrval  42415  pell1234qrval  42417  rpnnen3  42600  fnwe2lem1  42621  pwssplit4  42660  pwslnmlem2  42664  dgraaval  42715  itgoval  42732  rgspnval  42739  proot1hash  42770  rp-intrabeq  42796  rp-unirabeq  42797  rfovfvd  43579  rfovfvfvd  43580  rfovcnvf1od  43581  fsovrfovd  43586  fsovfvd  43587  fsovfvfvd  43588  fsovcnvlem  43590  nzss  43901  supminfxr  44989  dvnprodlem1  45477  dvnprodlem2  45478  dvnprodlem3  45479  dvnprod  45480  stoweidlem26  45557  stoweidlem27  45558  stoweidlem31  45562  stoweidlem34  45565  stoweidlem46  45577  fourierdlem79  45716  fourierdlem96  45733  fourierdlem97  45734  fourierdlem98  45735  fourierdlem99  45736  fourierdlem105  45742  fourierdlem107  45744  fourierdlem108  45745  fourierdlem110  45747  etransclem11  45776  salgenval  45852  subsaliuncl  45889  ovnval  46072  ovnval2  46076  ovnval2b  46083  ovncvrrp  46095  ovnsubaddlem1  46101  ovnsubadd  46103  ovncvr2  46142  hspmbl  46160  ovolval2  46175  ovnovollem3  46189  salpreimagelt  46238  salpreimalegt  46240  salpreimagtge  46256  salpreimaltle  46257  issmflem  46258  issmf  46259  salpreimagtlt  46261  smfpreimalt  46262  smfpreimaltf  46267  issmfle  46276  smfpimltxr  46278  smfpreimale  46285  issmfgt  46287  smfpreimagt  46293  issmfge  46301  smflimlem3  46304  smflimlem4  46305  smflim  46308  smfpimgtxr  46311  smfpreimage  46313  fvmptrabdm  46816  elsetpreimafveq  46879  prmdvdsfmtnof1  47069  fppr  47208  dfclnbgr2  47305  dfclnbgr3  47307  dfsclnbgr6  47335  bigoval  47813  line  47996  rrxline  47998  sphere  48011  line2y  48019  inpw  48080