Theorem rabbidv 3420

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rab 3414

This theorem is used by:  difeq2  4068  seex  5610  mptiniseg  6233  dfpred3g  6309  iunpreima  7060  elovmporab  7659  elovmpt3rab1  7673  naddcllem  8669  naddov2  8672  naddcom  8676  naddrid  8677  naddass  8690  fineqvlem  9241  mapfien2  9385  supeq1  9421  supeq2  9424  supeq3  9425  oieq1  9490  oieq2  9491  ordtypecbv  9495  ordtypelem3  9498  harval  9538  inf3lema  9609  wemapwe  9682  oef1o  9683  tz9.12lem3  9779  rankvalb  9787  rankvalg  9807  ranksnb  9818  rankonidlem  9819  cardval3  10014  cardidm  10021  alephsuc2  10140  coftr  10332  fin1a2lem11  10469  fin1a2lem12  10470  hsmex  10491  axdc3lem2  10510  zorn2lem1  10555  zorn2lem6  10560  zorn2lem7  10561  zorn2g  10562  wuncval  10808  tskmval  10905  peano5uzti  12770  uzval  12948  rpnnen1  13092  ixxval  13465  fzval  13622  hashbclem  14577  hashbc  14578  shftfn  15206  bitsfval  16573  sadfval  16602  sadcom  16613  smufval  16627  smupp1  16630  smupval  16638  smumullem  16642  gcdval  16646  bezoutlem2  16693  bezoutlem4  16695  lcmval  16747  lcmfval  16776  lcmf0val  16777  lcmfpr  16782  isprm  16828  odzval  16949  pcval  17002  pceulem  17003  pceu  17004  pczpre  17005  pcdiv  17010  prmreclem1  17074  prmreclem4  17077  prmreclem5  17078  ramval  17166  cshws0  17259  imasdsval  17667  mrcval  17764  eldmcoa  18220  chneq1  18766  cycsubg2  19405  cntzval  19515  cntzsnval  19518  odfval  19726  odfvalALT  19727  odval  19728  gexval  19772  efgsfo  19933  dprdval  20199  ablfac1a  20265  ablfac1b  20266  ablfac1eu  20269  ablfaclem1  20281  ablfaclem3  20283  rnghmval  20650  rhmval0  20685  rgspnval  20844  lspval  21230  ocvval  21953  dsmmelbas  22025  frlmsslss  22060  aspval  22160  psrass1lem  22221  psrmulval  22232  mplmonmul  22325  mhpval  22440  mhpmulcl  22450  coe1mul2  22568  pmatcoe1fsupp  22999  istopon  23210  toponsspwpw  23220  clsval  23335  neival  23400  ordtbaslem  23486  ordtbas2  23489  ordtopn1  23492  ordtopn2  23493  cnpval  23534  llyeq  23769  nllyeq  23770  ptfinfin  23818  finlocfin  23819  dissnlocfin  23828  locfindis  23829  xkoopn  23888  kqfval  24022  tsmsfbas  24427  blvalps  24684  blval  24685  nmofval  25013  nmoval  25014  ishtpy  25273  minveclem3b  25729  minveclem3  25730  minveclem4  25733  minveclem5  25734  ovolval  25774  vitalilem2  25910  vitalilem3  25911  vitalilem4  25912  vitali  25914  itg2monolem1  26051  elcpn  26234  mdegmullem  26376  elqaalem1  26624  elqaalem2  26625  elqaalem3  26626  elqaa  26627  aannenlem1  26637  aannenlem2  26638  jensen  27298  vmaval  27422  muval  27441  sgmval  27451  fsumdvdscom  27494  musum  27500  muinv  27502  dchrisum0fval  27814  dchrisum0ff  27816  logsqvma2  27852  pntrlog2bndlem1  27886  cutsval  28148  bdayons  28644  tglngval  28996  plngval  29237  ttgval  29434  ttgitvval  29441  ebtwntg  29542  numedglnl  29704  dfnbgr2  29900  dfnbgr3  29901  uvtxusgr  29965  vtxdgval  30031  rusgrnumwrdl2  30149  iswwlksnon  30424  rusgrnumwwlks  30548  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  clwlknf1oclwwlknlem2  30655  clwwlknon  30663  clwwlk0on0  30665  eupth2  30822  fusgreg2wsplem  30916  fusgreghash2wsp  30921  numclwlk1lem1  30952  sspval  31307  ubthlem1  31454  ubthlem2  31455  ubthlem3  31456  ocval  31864  spanval  31917  chsupid  31996  eigvecval  32480  specval  32482  fcobijfs2  33296  pwrssmgc  33543  fxpgaval  33710  nsgqusf1olem3  33948  selvply1rhmlemb  34133  mplvrpmrhm  34161  psrmonmul  34164  esplyfval  34177  esplyfval0  34178  minplyval  34319  constrsuc  34352  constrcbvlem  34369  crefeq  34459  zarcls1  34483  zarclsun  34484  zarclsiin  34485  zarclsint  34486  zarclssn  34487  zartop  34490  zartopon  34491  zart0  34493  zarmxt1  34494  zarcmp  34496  rhmpreimacnlem  34498  rhmpreimacn  34499  ordtcnvNEW  34534  ordtrest2NEW  34537  ordtconnlem1  34538  measvuni  34829  brfae  34863  omsfval  34909  orvcelval  35084  ballotlemi  35116  bnj602  35528  fineqvnttrclselem2  35763  fineqvnttrclselem3  35764  fineqvnttrclse  35765  onvf1odlem3  35857  subfacp1lem6  35919  kur14  35950  cvmscbv  35992  cvmsi  35999  cvmsval  36000  snmlval  36065  snmlflim  36066  satfv0  36092  satfv1  36097  satfv0fun  36105  satffunlem1lem1  36136  satffunlem2lem1  36138  satfv0fvfmla0  36147  satfv1fvfmla1  36157  prv1n  36165  fvray  36876  fwddifnval  36898  nmulprop  36909  nmulcom  36913  neibastop3  37120  weiunlem  37221  icoreval  38244  fin2so  38498  poimirlem26  38532  poimirlem27  38533  poimirlem28  38534  poimirlem32  38538  ftc1anclem6  38584  islinei  40765  pmapval  40782  paddval  40823  paddcom  40838  pclvalN  40915  ldilset  41134  dilsetN  41178  diafval  42056  diaval  42057  docavalN  42148  dicfval  42200  dochfval  42375  dochval  42376  mapdval  42653  mapdsn2  42667  grpods  43212  unitscyglem1  43213  unitscyglem2  43214  unitscyglem3  43215  unitscyglem4  43216  prjcrvval  43622  2rexfrabdioph  43756  3rexfrabdioph  43757  4rexfrabdioph  43758  6rexfrabdioph  43759  7rexfrabdioph  43760  eldioph4i  43772  diophren  43773  pell1qrval  43806  pell14qrval  43808  pell1234qrval  43810  rpnnen3  43992  fnwe2lem1  44010  pwssplit4  44049  pwslnmlem2  44053  dgraaval  44104  itgoval  44121  proot1hash  44155  rp-intrabeq  44181  rp-unirabeq  44182  rfovfvd  44961  rfovfvfvd  44962  rfovcnvf1od  44963  fsovrfovd  44968  fsovfvd  44969  fsovfvfvd  44970  fsovcnvlem  44972  nzss  45260  supminfxr  46418  dvnprodlem1  46900  dvnprodlem2  46901  dvnprodlem3  46902  dvnprod  46903  stoweidlem26  46980  stoweidlem27  46981  stoweidlem31  46985  stoweidlem34  46988  stoweidlem46  47000  fourierdlem79  47139  fourierdlem96  47156  fourierdlem97  47157  fourierdlem98  47158  fourierdlem99  47159  fourierdlem105  47165  fourierdlem107  47167  fourierdlem108  47168  fourierdlem110  47170  etransclem11  47199  salgenval  47275  subsaliuncl  47312  ovnval  47495  ovnval2  47499  ovnval2b  47506  ovncvrrp  47518  ovnsubaddlem1  47524  ovnsubadd  47526  ovncvr2  47565  hspmbl  47583  ovolval2  47598  ovnovollem3  47612  salpreimagelt  47661  salpreimalegt  47663  salpreimagtge  47679  salpreimaltle  47680  issmflem  47681  issmf  47682  salpreimagtlt  47684  smfpreimalt  47685  smfpreimaltf  47690  issmfle  47699  smfpimltxr  47701  smfpreimale  47708  issmfgt  47710  smfpreimagt  47716  issmfge  47724  smflimlem3  47727  smflimlem4  47728  smflim  47731  smfpimgtxr  47734  smfpreimage  47736  tmachlem-agreeself  47890  tmachlem-agreeprod  47891  fvmptrabdm  48307  elsetpreimafveq  48423  prmdvdsfmtnof1  48616  fppr  48768  dfclnbgr2  48865  dfclnbgr3  48868  dfsclnbgr6  48900  grlimedgclnbgr  49037  grlimgrtri  49045  grilcbri2  49053  bigoval  49605  line  49788  rrxline  49790  sphere  49803  line2y  49811  inpw  49879