Theorem rabbidv 3413

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-rab 3406

This theorem is referenced by:  difeq2  4081  seex  5600  mptiniseg  6196  dfpred3g  6270  elovmporab  7604  elovmpt3rab1  7618  naddcllem  8627  naddov2  8630  naddcom  8633  naddrid  8634  naddass  8647  fineqvlem  9213  mapfien2  9354  supeq1  9390  supeq2  9393  supeq3  9394  oieq1  9457  oieq2  9458  ordtypecbv  9462  ordtypelem3  9465  harval  9505  inf3lema  9569  wemapwe  9642  oef1o  9643  tz9.12lem3  9734  rankvalb  9742  rankvalg  9762  ranksnb  9772  rankonidlem  9773  cardval3  9897  cardidm  9904  alephsuc2  10025  coftr  10218  fin1a2lem11  10355  fin1a2lem12  10356  hsmex  10377  axdc3lem2  10396  zorn2lem1  10441  zorn2lem6  10446  zorn2lem7  10447  zorn2g  10448  wuncval  10687  tskmval  10784  peano5uzti  12602  uzval  12774  rpnnen1  12917  ixxval  13282  fzval  13436  hashbclem  14361  hashbc  14362  shftfn  14970  bitsfval  16314  sadfval  16343  sadcom  16354  smufval  16368  smupp1  16371  smupval  16379  smumullem  16383  gcdval  16387  bezoutlem2  16432  bezoutlem4  16434  lcmval  16479  lcmfval  16508  lcmf0val  16509  lcmfpr  16514  isprm  16560  odzval  16674  pcval  16727  pceulem  16728  pceu  16729  pczpre  16730  pcdiv  16735  prmreclem1  16799  prmreclem4  16802  prmreclem5  16803  ramval  16891  cshws0  16985  imasdsval  17411  mrcval  17504  eldmcoa  17965  cycsubg2  19017  cntzval  19115  cntzsnval  19118  odfval  19328  odfvalALT  19329  odval  19330  gexval  19374  efgsfo  19535  dprdval  19796  ablfac1a  19862  ablfac1b  19863  ablfac1eu  19866  ablfaclem1  19878  ablfaclem3  19880  lspval  20493  ocvval  21108  dsmmelbas  21182  frlmsslss  21217  aspval  21313  psrass1lemOLD  21379  psrass1lem  21382  psrmulval  21391  mplmonmul  21474  mhpval  21567  mhpmulcl  21576  coe1mul2  21677  pmatcoe1fsupp  22087  istopon  22298  toponsspwpw  22308  clsval  22425  neival  22490  ordtbaslem  22576  ordtbas2  22579  ordtopn1  22582  ordtopn2  22583  cnpval  22624  llyeq  22858  nllyeq  22859  ptfinfin  22907  finlocfin  22908  dissnlocfin  22917  locfindis  22918  xkoopn  22977  kqfval  23111  tsmsfbas  23516  blvalps  23775  blval  23776  nmofval  24115  nmoval  24116  ishtpy  24372  minveclem3b  24829  minveclem3  24830  minveclem4  24833  minveclem5  24834  ovolval  24874  vitalilem2  25010  vitalilem3  25011  vitalilem4  25012  vitali  25014  itg2monolem1  25152  elcpn  25335  mdegmullem  25480  elqaalem1  25716  elqaalem2  25717  elqaalem3  25718  elqaa  25719  aannenlem1  25725  aannenlem2  25726  jensen  26375  vmaval  26499  muval  26518  sgmval  26528  fsumdvdscom  26571  musum  26577  muinv  26579  dchrisum0fval  26890  dchrisum0ff  26892  logsqvma2  26928  pntrlog2bndlem1  26962  scutval  27182  tglngval  27556  ttgval  27880  ttgvalOLD  27881  ttgitvval  27893  ebtwntg  27994  numedglnl  28158  dfnbgr2  28348  dfnbgr3  28349  uvtxusgr  28413  vtxdgval  28479  rusgrnumwrdl2  28597  iswwlksnon  28861  rusgrnumwwlks  28982  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  clwlknf1oclwwlknlem2  29089  clwwlknon  29097  clwwlk0on0  29099  eupth2  29246  fusgreg2wsplem  29340  fusgreghash2wsp  29345  numclwlk1lem1  29376  sspval  29728  ubthlem1  29875  ubthlem2  29876  ubthlem3  29877  ocval  30285  spanval  30338  chsupid  30417  eigvecval  30901  specval  30903  iunpreima  31550  pwrssmgc  31930  nsgqusf1olem3  32267  minplyval  32461  crefeq  32515  zarcls1  32539  zarclsun  32540  zarclsiin  32541  zarclsint  32542  zarclssn  32543  zartop  32546  zartopon  32547  zart0  32549  zarmxt1  32550  zarcmp  32552  rhmpreimacnlem  32554  rhmpreimacn  32555  ordtcnvNEW  32590  ordtrest2NEW  32593  ordtconnlem1  32594  measvuni  32902  brfae  32936  omsfval  32983  orvcelval  33157  ballotlemi  33189  bnj602  33616  subfacp1lem6  33866  kur14  33897  cvmscbv  33939  cvmsi  33946  cvmsval  33947  snmlval  34012  snmlflim  34013  satfv0  34039  satfv1  34044  satfv0fun  34052  satffunlem1lem1  34083  satffunlem2lem1  34085  satfv0fvfmla0  34094  satfv1fvfmla1  34104  prv1n  34112  fvray  34802  fwddifnval  34824  neibastop3  34910  icoreval  35897  fin2so  36138  poimirlem26  36177  poimirlem27  36178  poimirlem28  36179  poimirlem32  36183  ftc1anclem6  36229  islinei  38276  pmapval  38293  paddval  38334  paddcom  38349  pclvalN  38426  ldilset  38645  dilsetN  38689  diafval  39567  diaval  39568  docavalN  39659  dicfval  39711  dochfval  39886  dochval  39887  mapdval  40164  mapdsn2  40178  prjcrvval  41028  2rexfrabdioph  41177  3rexfrabdioph  41178  4rexfrabdioph  41179  6rexfrabdioph  41180  7rexfrabdioph  41181  eldioph4i  41193  diophren  41194  pell1qrval  41227  pell14qrval  41229  pell1234qrval  41231  rpnnen3  41414  fnwe2lem1  41435  pwssplit4  41474  pwslnmlem2  41478  dgraaval  41529  itgoval  41546  rgspnval  41553  proot1hash  41585  rp-intrabeq  41613  rp-unirabeq  41614  rfovfvd  42396  rfovfvfvd  42397  rfovcnvf1od  42398  fsovrfovd  42403  fsovfvd  42404  fsovfvfvd  42405  fsovcnvlem  42407  nzss  42719  supminfxr  43819  dvnprodlem1  44307  dvnprodlem2  44308  dvnprodlem3  44309  dvnprod  44310  stoweidlem26  44387  stoweidlem27  44388  stoweidlem31  44392  stoweidlem34  44395  stoweidlem46  44407  fourierdlem79  44546  fourierdlem96  44563  fourierdlem97  44564  fourierdlem98  44565  fourierdlem99  44566  fourierdlem105  44572  fourierdlem107  44574  fourierdlem108  44575  fourierdlem110  44577  etransclem11  44606  salgenval  44682  subsaliuncl  44719  ovnval  44902  ovnval2  44906  ovnval2b  44913  ovncvrrp  44925  ovnsubaddlem1  44931  ovnsubadd  44933  ovncvr2  44972  hspmbl  44990  ovolval2  45005  ovnovollem3  45019  salpreimagelt  45068  salpreimalegt  45070  salpreimagtge  45086  salpreimaltle  45087  issmflem  45088  issmf  45089  salpreimagtlt  45091  smfpreimalt  45092  smfpreimaltf  45097  issmfle  45106  smfpimltxr  45108  smfpreimale  45115  issmfgt  45117  smfpreimagt  45123  issmfge  45131  smflimlem3  45134  smflimlem4  45135  smflim  45138  smfpimgtxr  45141  smfpreimage  45143  fvmptrabdm  45645  elsetpreimafveq  45709  prmdvdsfmtnof1  45899  fppr  46038  rnghmval  46309  bigoval  46755  line  46938  rrxline  46940  sphere  46953  line2y  46961  inpw  47023