Theorem rabbidv 3424

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ∈ wcel 2145  {crab 3417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-rab 3418

This theorem is referenced by:  difeq2  4077  seex  5611  mptiniseg  6230  dfpred3g  6304  elovmporab  7646  elovmpt3rab1  7660  naddcllem  8650  naddov2  8653  naddcom  8657  naddrid  8658  naddass  8671  fineqvlem  9214  mapfien2  9357  supeq1  9393  supeq2  9396  supeq3  9397  oieq1  9462  oieq2  9463  ordtypecbv  9467  ordtypelem3  9470  harval  9510  inf3lema  9581  wemapwe  9654  oef1o  9655  tz9.12lem3  9749  rankvalb  9757  rankvalg  9777  ranksnb  9787  rankonidlem  9788  cardval3  9926  cardidm  9933  alephsuc2  10052  coftr  10245  fin1a2lem11  10382  fin1a2lem12  10383  hsmex  10404  axdc3lem2  10423  zorn2lem1  10468  zorn2lem6  10473  zorn2lem7  10474  zorn2g  10475  wuncval  10715  tskmval  10812  peano5uzti  12677  uzval  12855  rpnnen1  12998  ixxval  13371  fzval  13528  hashbclem  14479  hashbc  14480  shftfn  15100  bitsfval  16471  sadfval  16500  sadcom  16511  smufval  16525  smupp1  16528  smupval  16536  smumullem  16540  gcdval  16544  bezoutlem2  16588  bezoutlem4  16590  lcmval  16640  lcmfval  16669  lcmf0val  16670  lcmfpr  16675  isprm  16721  odzval  16841  pcval  16894  pceulem  16895  pceu  16896  pczpre  16897  pcdiv  16902  prmreclem1  16966  prmreclem4  16969  prmreclem5  16970  ramval  17058  cshws0  17151  imasdsval  17559  mrcval  17656  eldmcoa  18112  chneq1  18658  cycsubg2  19272  cntzval  19382  cntzsnval  19385  odfval  19593  odfvalALT  19594  odval  19595  gexval  19639  efgsfo  19800  dprdval  20066  ablfac1a  20132  ablfac1b  20133  ablfac1eu  20136  ablfaclem1  20148  ablfaclem3  20150  rnghmval  20513  rgspnval  20688  lspval  21065  ocvval  21777  dsmmelbas  21849  frlmsslss  21884  aspval  21982  psrass1lem  22043  psrmulval  22054  mplmonmul  22147  mhpval  22262  mhpmulcl  22272  coe1mul2  22390  pmatcoe1fsupp  22819  istopon  23030  toponsspwpw  23040  clsval  23155  neival  23220  ordtbaslem  23306  ordtbas2  23309  ordtopn1  23312  ordtopn2  23313  cnpval  23354  llyeq  23588  nllyeq  23589  ptfinfin  23637  finlocfin  23638  dissnlocfin  23647  locfindis  23648  xkoopn  23707  kqfval  23841  tsmsfbas  24246  blvalps  24503  blval  24504  nmofval  24832  nmoval  24833  ishtpy  25092  minveclem3b  25548  minveclem3  25549  minveclem4  25552  minveclem5  25553  ovolval  25593  vitalilem2  25729  vitalilem3  25730  vitalilem4  25731  vitali  25733  itg2monolem1  25870  elcpn  26054  mdegmullem  26196  elqaalem1  26441  elqaalem2  26442  elqaalem3  26443  elqaa  26444  aannenlem1  26450  aannenlem2  26451  jensen  27111  vmaval  27235  muval  27254  sgmval  27264  fsumdvdscom  27307  musum  27313  muinv  27315  dchrisum0fval  27627  dchrisum0ff  27629  logsqvma2  27665  pntrlog2bndlem1  27699  cutsval  27931  bdayons  28427  tglngval  28778  plngval  29007  ttgval  29133  ttgitvval  29140  ebtwntg  29241  numedglnl  29403  dfnbgr2  29596  dfnbgr3  29597  uvtxusgr  29661  vtxdgval  29727  rusgrnumwrdl2  29845  iswwlksnon  30111  rusgrnumwwlks  30235  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  clwlknf1oclwwlknlem2  30342  clwwlknon  30350  clwwlk0on0  30352  eupth2  30499  fusgreg2wsplem  30593  fusgreghash2wsp  30598  numclwlk1lem1  30629  sspval  30984  ubthlem1  31131  ubthlem2  31132  ubthlem3  31133  ocval  31541  spanval  31594  chsupid  31673  eigvecval  32157  specval  32159  iunpreima  32819  fcobijfs2  32979  pwrssmgc  33233  fxpgaval  33400  nsgqusf1olem3  33640  selvply1rhmlemb  33826  mplvrpmrhm  33854  psrmonmul  33857  esplyfval  33870  esplyfval0  33871  minplyval  34012  constrsuc  34045  constrcbvlem  34062  crefeq  34152  zarcls1  34176  zarclsun  34177  zarclsiin  34178  zarclsint  34179  zarclssn  34180  zartop  34183  zartopon  34184  zart0  34186  zarmxt1  34187  zarcmp  34189  rhmpreimacnlem  34191  rhmpreimacn  34192  ordtcnvNEW  34227  ordtrest2NEW  34230  ordtconnlem1  34231  measvuni  34521  brfae  34555  omsfval  34601  orvcelval  34776  ballotlemi  34808  bnj602  35220  fineqvnttrclselem2  35430  fineqvnttrclselem3  35431  fineqvnttrclse  35432  onvf1odlem3  35460  subfacp1lem6  35548  kur14  35579  cvmscbv  35621  cvmsi  35628  cvmsval  35629  snmlval  35694  snmlflim  35695  satfv0  35721  satfv1  35726  satfv0fun  35734  satffunlem1lem1  35765  satffunlem2lem1  35767  satfv0fvfmla0  35776  satfv1fvfmla1  35786  prv1n  35794  fvray  36504  fwddifnval  36526  nmulprop  36553  nmulcom  36557  neibastop3  36735  weiunlem  36836  icoreval  37859  fin2so  38118  poimirlem26  38157  poimirlem27  38158  poimirlem28  38159  poimirlem32  38163  ftc1anclem6  38209  islinei  40376  pmapval  40393  paddval  40434  paddcom  40449  pclvalN  40526  ldilset  40745  dilsetN  40789  diafval  41667  diaval  41668  docavalN  41759  dicfval  41811  dochfval  41986  dochval  41987  mapdval  42264  mapdsn2  42278  grpods  42823  unitscyglem1  42824  unitscyglem2  42825  unitscyglem3  42826  unitscyglem4  42827  prjcrvval  43226  2rexfrabdioph  43385  3rexfrabdioph  43386  4rexfrabdioph  43387  6rexfrabdioph  43388  7rexfrabdioph  43389  eldioph4i  43401  diophren  43402  pell1qrval  43435  pell14qrval  43437  pell1234qrval  43439  rpnnen3  43621  fnwe2lem1  43639  pwssplit4  43678  pwslnmlem2  43682  dgraaval  43733  itgoval  43750  proot1hash  43784  rp-intrabeq  43810  rp-unirabeq  43811  rfovfvd  44590  rfovfvfvd  44591  rfovcnvf1od  44592  fsovrfovd  44597  fsovfvd  44598  fsovfvfvd  44599  fsovcnvlem  44601  nzss  44891  supminfxr  46036  dvnprodlem1  46518  dvnprodlem2  46519  dvnprodlem3  46520  dvnprod  46521  stoweidlem26  46598  stoweidlem27  46599  stoweidlem31  46603  stoweidlem34  46606  stoweidlem46  46618  fourierdlem79  46757  fourierdlem96  46774  fourierdlem97  46775  fourierdlem98  46776  fourierdlem99  46777  fourierdlem105  46783  fourierdlem107  46785  fourierdlem108  46786  fourierdlem110  46788  etransclem11  46817  salgenval  46893  subsaliuncl  46930  ovnval  47113  ovnval2  47117  ovnval2b  47124  ovncvrrp  47136  ovnsubaddlem1  47142  ovnsubadd  47144  ovncvr2  47183  hspmbl  47201  ovolval2  47216  ovnovollem3  47230  salpreimagelt  47279  salpreimalegt  47281  salpreimagtge  47297  salpreimaltle  47298  issmflem  47299  issmf  47300  salpreimagtlt  47302  smfpreimalt  47303  smfpreimaltf  47308  issmfle  47317  smfpimltxr  47319  smfpreimale  47326  issmfgt  47328  smfpreimagt  47334  issmfge  47342  smflimlem3  47345  smflimlem4  47346  smflim  47349  smfpimgtxr  47352  smfpreimage  47354  fvmptrabdm  47885  elsetpreimafveq  48001  prmdvdsfmtnof1  48194  fppr  48346  dfclnbgr2  48443  dfclnbgr3  48446  dfsclnbgr6  48478  grlimedgclnbgr  48615  grlimgrtri  48623  grilcbri2  48631  bigoval  49180  line  49363  rrxline  49365  sphere  49378  line2y  49386  inpw  49454