Theorem rabbidv 3419

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-rab 3413

This theorem is used by:  difeq2  4057  seex  5609  mptiniseg  6240  dfpred3g  6316  iunpreima  7069  elovmporab  7668  elovmpt3rab1  7682  fnwe2lem2  8149  naddcllem  8689  naddov2  8692  naddcom  8696  naddrid  8697  naddass  8710  fineqvlem  9261  mapfien2  9405  supeq1  9441  supeq2  9444  supeq3  9445  oieq1  9510  oieq2  9511  ordtypecbv  9515  ordtypelem3  9518  harval  9558  inf3lema  9629  wemapwe  9702  oef1o  9703  tz9.12lem3  9800  rankvalb  9809  rankvalg  9830  ranksnb  9841  rankonidlem  9842  cardval3  10037  cardidm  10044  alephsuc2  10163  coftr  10355  fin1a2lem11  10492  fin1a2lem12  10493  hsmex  10514  axdc3lem2  10533  zorn2lem1  10578  zorn2lem6  10583  zorn2lem7  10584  zorn2g  10585  wuncval  10831  tskmval  10928  peano5uzti  12793  uzval  12971  rpnnen1  13115  ixxval  13488  fzval  13645  hashbclem  14601  hashbc  14602  shftfn  15232  bitsfval  16599  sadfval  16628  sadcom  16639  smufval  16653  smupp1  16656  smupval  16664  smumullem  16668  gcdval  16672  bezoutlem2  16719  bezoutlem4  16721  lcmval  16773  lcmfval  16802  lcmf0val  16803  lcmfpr  16808  isprm  16854  odzval  16975  pcval  17028  pceulem  17029  pceu  17030  pczpre  17031  pcdiv  17036  prmreclem1  17100  prmreclem4  17103  prmreclem5  17104  ramval  17192  cshws0  17285  imasdsval  17693  mrcval  17790  eldmcoa  18246  chneq1  18792  cycsubg2  19431  cntzval  19541  cntzsnval  19544  odfval  19752  odfvalALT  19753  odval  19754  gexval  19798  efgsfo  19959  dprdval  20225  ablfac1a  20291  ablfac1b  20292  ablfac1eu  20295  ablfaclem1  20307  ablfaclem3  20309  rnghmval  20676  rhmval0  20711  rgspnval  20870  lspval  21256  ocvval  21979  dsmmelbas  22051  frlmsslss  22086  aspval  22186  psrass1lem  22247  psrmulval  22258  mplmonmul  22351  mhpval  22466  mhpmulcl  22476  coe1mul2  22594  pmatcoe1fsupp  23025  istopon  23236  toponsspwpw  23246  clsval  23361  neival  23426  ordtbaslem  23512  ordtbas2  23515  ordtopn1  23518  ordtopn2  23519  cnpval  23560  llyeq  23795  nllyeq  23796  ptfinfin  23844  finlocfin  23845  dissnlocfin  23854  locfindis  23855  xkoopn  23914  kqfval  24048  tsmsfbas  24453  blvalps  24710  blval  24711  nmofval  25039  nmoval  25040  ishtpy  25299  minveclem3b  25755  minveclem3  25756  minveclem4  25759  minveclem5  25760  ovolval  25800  vitalilem2  25936  vitalilem3  25937  vitalilem4  25938  vitali  25940  itg2monolem1  26077  elcpn  26260  mdegmullem  26402  elqaalem1  26648  elqaalem2  26649  elqaalem3  26650  elqaa  26651  aannenlem1  26661  aannenlem2  26662  jensen  27322  vmaval  27446  muval  27465  sgmval  27475  fsumdvdscom  27518  musum  27524  muinv  27526  dchrisum0fval  27838  dchrisum0ff  27840  logsqvma2  27876  pntrlog2bndlem1  27910  cutsval  28172  bdayons  28668  tglngval  29020  plngval  29261  ttgval  29458  ttgitvval  29465  ebtwntg  29566  numedglnl  29728  dfnbgr2  29924  dfnbgr3  29925  uvtxusgr  29989  vtxdgval  30055  rusgrnumwrdl2  30173  iswwlksnon  30448  rusgrnumwwlks  30572  hashecclwwlkn1  30674  umgrhashecclwwlk  30675  clwlknf1oclwwlknlem2  30679  clwwlknon  30687  clwwlk0on0  30689  eupth2  30846  fusgreg2wsplem  30940  fusgreghash2wsp  30945  numclwlk1lem1  30976  sspval  31331  ubthlem1  31478  ubthlem2  31479  ubthlem3  31480  ocval  31888  spanval  31941  chsupid  32020  eigvecval  32504  specval  32506  fcobijfs2  33361  pwrssmgc  33608  fxpgaval  33775  nsgqusf1olem3  34013  selvply1rhmlemb  34198  mplvrpmrhm  34226  psrmonmul  34229  esplyfval  34242  esplyfval0  34243  minplyval  34384  constrsuc  34417  constrcbvlem  34434  crefeq  34524  zarcls1  34548  zarclsun  34549  zarclsiin  34550  zarclsint  34551  zarclssn  34552  zartop  34555  zartopon  34556  zart0  34558  zarmxt1  34559  zarcmp  34561  rhmpreimacnlem  34563  rhmpreimacn  34564  ordtcnvNEW  34599  ordtrest2NEW  34602  ordtconnlem1  34603  measvuni  34894  brfae  34928  omsfval  34973  orvcelval  35148  ballotlemi  35180  bnj602  35592  werankwe  35792  werankwe2  35793  rankse  35794  fineqvnttrclselem2  35847  fineqvnttrclselem3  35848  fineqvnttrclse  35849  onvf1odlem3  35953  onprcf1acwevdlem2  35966  onf1oracwevd  35972  subfacp1lem6  36037  kur14  36068  cvmscbv  36110  cvmsi  36117  cvmsval  36118  snmlval  36183  snmlflim  36184  satfv0  36210  satfv1  36215  satfv0fun  36223  satffunlem1lem1  36254  satffunlem2lem1  36256  satfv0fvfmla0  36265  satfv1fvfmla1  36275  prv1n  36283  fvray  36999  fwddifnval  37021  nmulprop  37032  nmulcom  37036  neibastop3  37243  weiunlem  37344  icoreval  38370  fin2so  38624  poimirlem26  38658  poimirlem27  38659  poimirlem28  38660  poimirlem32  38664  ftc1anclem6  38710  islinei  40891  pmapval  40908  paddval  40949  paddcom  40964  pclvalN  41041  ldilset  41260  dilsetN  41304  diafval  42182  diaval  42183  docavalN  42274  dicfval  42326  dochfval  42501  dochval  42502  mapdval  42779  mapdsn2  42793  grpods  43338  unitscyglem1  43339  unitscyglem2  43340  unitscyglem3  43341  unitscyglem4  43342  frlmnzcoordval  43747  prjcrvval  43762  2rexfrabdioph  43897  3rexfrabdioph  43898  4rexfrabdioph  43899  6rexfrabdioph  43900  7rexfrabdioph  43901  eldioph4i  43913  diophren  43914  pell1qrval  43947  pell14qrval  43949  pell1234qrval  43951  rpnnen3  44133  pwssplit4  44185  pwslnmlem2  44189  dgraaval  44240  itgoval  44257  proot1hash  44291  rp-intrabeq  44317  rp-unirabeq  44318  rfovfvd  45096  rfovfvfvd  45097  rfovcnvf1od  45098  fsovrfovd  45103  fsovfvd  45104  fsovfvfvd  45105  fsovcnvlem  45107  nzss  45395  supminfxr  46568  dvnprodlem1  47050  dvnprodlem2  47051  dvnprodlem3  47052  dvnprod  47053  stoweidlem26  47130  stoweidlem27  47131  stoweidlem31  47135  stoweidlem34  47138  stoweidlem46  47150  fourierdlem79  47289  fourierdlem96  47306  fourierdlem97  47307  fourierdlem98  47308  fourierdlem99  47309  fourierdlem105  47315  fourierdlem107  47317  fourierdlem108  47318  fourierdlem110  47320  etransclem11  47349  salgenval  47425  subsaliuncl  47462  ovnval  47645  ovnval2  47649  ovnval2b  47656  ovncvrrp  47668  ovnsubaddlem1  47674  ovnsubadd  47676  ovncvr2  47715  hspmbl  47733  ovolval2  47748  ovnovollem3  47762  salpreimagelt  47811  salpreimalegt  47813  salpreimagtge  47829  salpreimaltle  47830  issmflem  47831  issmf  47832  salpreimagtlt  47834  smfpreimalt  47835  smfpreimaltf  47840  issmfle  47849  smfpimltxr  47851  smfpreimale  47858  issmfgt  47860  smfpreimagt  47866  issmfge  47874  smflimlem3  47877  smflimlem4  47878  smflim  47881  smfpimgtxr  47884  smfpreimage  47886  tmachlem-agreeself  48040  tmachlem-agreeprod  48041  fvmptrabdm  48457  elsetpreimafveq  48573  prmdvdsfmtnof1  48766  fppr  48918  dfclnbgr2  49015  dfclnbgr3  49018  dfsclnbgr6  49050  grlimedgclnbgr  49187  grlimgrtri  49195  grilcbri2  49203  bigoval  49755  line  49939  rrxline  49941  sphere  49953  line2y  49961  inpw  50030