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

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

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 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-rab 3420

This theorem is used by:  difeq2  4078  seex  5625  mptiniseg  6245  dfpred3g  6321  elovmporab  7669  elovmpt3rab1  7683  naddcllem  8671  naddov2  8674  naddcom  8678  naddrid  8679  naddass  8692  fineqvlem  9236  mapfien2  9379  supeq1  9415  supeq2  9418  supeq3  9419  oieq1  9484  oieq2  9485  ordtypecbv  9489  ordtypelem3  9492  harval  9532  inf3lema  9603  wemapwe  9676  oef1o  9677  tz9.12lem3  9771  rankvalb  9779  rankvalg  9799  ranksnb  9809  rankonidlem  9810  cardval3  9957  cardidm  9964  alephsuc2  10083  coftr  10275  fin1a2lem11  10412  fin1a2lem12  10413  hsmex  10434  axdc3lem2  10453  zorn2lem1  10498  zorn2lem6  10503  zorn2lem7  10504  zorn2g  10505  wuncval  10745  tskmval  10842  peano5uzti  12704  uzval  12882  rpnnen1  13025  ixxval  13398  fzval  13555  hashbclem  14509  hashbc  14510  shftfn  15136  bitsfval  16506  sadfval  16535  sadcom  16546  smufval  16560  smupp1  16563  smupval  16571  smumullem  16575  gcdval  16579  bezoutlem2  16623  bezoutlem4  16625  lcmval  16675  lcmfval  16704  lcmf0val  16705  lcmfpr  16710  isprm  16756  odzval  16876  pcval  16929  pceulem  16930  pceu  16931  pczpre  16932  pcdiv  16937  prmreclem1  17001  prmreclem4  17004  prmreclem5  17005  ramval  17093  cshws0  17186  imasdsval  17594  mrcval  17691  eldmcoa  18147  chneq1  18693  cycsubg2  19312  cntzval  19422  cntzsnval  19425  odfval  19633  odfvalALT  19634  odval  19635  gexval  19679  efgsfo  19840  dprdval  20106  ablfac1a  20172  ablfac1b  20173  ablfac1eu  20176  ablfaclem1  20188  ablfaclem3  20190  rnghmval  20555  rhmval0  20590  rgspnval  20748  lspval  21133  ocvval  21854  dsmmelbas  21926  frlmsslss  21961  aspval  22059  psrass1lem  22120  psrmulval  22131  mplmonmul  22224  mhpval  22339  mhpmulcl  22349  coe1mul2  22467  pmatcoe1fsupp  22895  istopon  23106  toponsspwpw  23116  clsval  23231  neival  23296  ordtbaslem  23382  ordtbas2  23385  ordtopn1  23388  ordtopn2  23389  cnpval  23430  llyeq  23664  nllyeq  23665  ptfinfin  23713  finlocfin  23714  dissnlocfin  23723  locfindis  23724  xkoopn  23783  kqfval  23917  tsmsfbas  24322  blvalps  24579  blval  24580  nmofval  24908  nmoval  24909  ishtpy  25168  minveclem3b  25624  minveclem3  25625  minveclem4  25628  minveclem5  25629  ovolval  25669  vitalilem2  25805  vitalilem3  25806  vitalilem4  25807  vitali  25809  itg2monolem1  25946  elcpn  26130  mdegmullem  26272  elqaalem1  26517  elqaalem2  26518  elqaalem3  26519  elqaa  26520  aannenlem1  26528  aannenlem2  26529  jensen  27190  vmaval  27314  muval  27333  sgmval  27343  fsumdvdscom  27386  musum  27392  muinv  27394  dchrisum0fval  27706  dchrisum0ff  27708  logsqvma2  27744  pntrlog2bndlem1  27778  cutsval  28010  bdayons  28506  tglngval  28857  plngval  29096  ttgval  29261  ttgitvval  29268  ebtwntg  29369  numedglnl  29531  dfnbgr2  29724  dfnbgr3  29725  uvtxusgr  29789  vtxdgval  29855  rusgrnumwrdl2  29973  iswwlksnon  30239  rusgrnumwwlks  30363  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  clwlknf1oclwwlknlem2  30470  clwwlknon  30478  clwwlk0on0  30480  eupth2  30627  fusgreg2wsplem  30721  fusgreghash2wsp  30726  numclwlk1lem1  30757  sspval  31112  ubthlem1  31259  ubthlem2  31260  ubthlem3  31261  ocval  31669  spanval  31722  chsupid  31801  eigvecval  32285  specval  32287  iunpreima  32946  fcobijfs2  33104  pwrssmgc  33351  fxpgaval  33518  nsgqusf1olem3  33755  selvply1rhmlemb  33940  mplvrpmrhm  33968  psrmonmul  33971  esplyfval  33984  esplyfval0  33985  minplyval  34126  constrsuc  34159  constrcbvlem  34176  crefeq  34266  zarcls1  34290  zarclsun  34291  zarclsiin  34292  zarclsint  34293  zarclssn  34294  zartop  34297  zartopon  34298  zart0  34300  zarmxt1  34301  zarcmp  34303  rhmpreimacnlem  34305  rhmpreimacn  34306  ordtcnvNEW  34341  ordtrest2NEW  34344  ordtconnlem1  34345  measvuni  34636  brfae  34670  omsfval  34716  orvcelval  34891  ballotlemi  34923  bnj602  35335  fineqvnttrclselem2  35559  fineqvnttrclselem3  35560  fineqvnttrclse  35561  onvf1odlem3  35613  subfacp1lem6  35698  kur14  35729  cvmscbv  35771  cvmsi  35778  cvmsval  35779  snmlval  35844  snmlflim  35845  satfv0  35871  satfv1  35876  satfv0fun  35884  satffunlem1lem1  35915  satffunlem2lem1  35917  satfv0fvfmla0  35926  satfv1fvfmla1  35936  prv1n  35944  fvray  36654  fwddifnval  36676  nmulprop  36703  nmulcom  36707  neibastop3  36914  weiunlem  37015  icoreval  38040  fin2so  38299  poimirlem26  38338  poimirlem27  38339  poimirlem28  38340  poimirlem32  38344  ftc1anclem6  38390  islinei  40555  pmapval  40572  paddval  40613  paddcom  40628  pclvalN  40705  ldilset  40924  dilsetN  40968  diafval  41846  diaval  41847  docavalN  41938  dicfval  41990  dochfval  42165  dochval  42166  mapdval  42443  mapdsn2  42457  grpods  43002  unitscyglem1  43003  unitscyglem2  43004  unitscyglem3  43005  unitscyglem4  43006  prjcrvval  43405  2rexfrabdioph  43564  3rexfrabdioph  43565  4rexfrabdioph  43566  6rexfrabdioph  43567  7rexfrabdioph  43568  eldioph4i  43580  diophren  43581  pell1qrval  43614  pell14qrval  43616  pell1234qrval  43618  rpnnen3  43800  fnwe2lem1  43818  pwssplit4  43857  pwslnmlem2  43861  dgraaval  43912  itgoval  43929  proot1hash  43963  rp-intrabeq  43989  rp-unirabeq  43990  rfovfvd  44769  rfovfvfvd  44770  rfovcnvf1od  44771  fsovrfovd  44776  fsovfvd  44777  fsovfvfvd  44778  fsovcnvlem  44780  nzss  45068  supminfxr  46219  dvnprodlem1  46701  dvnprodlem2  46702  dvnprodlem3  46703  dvnprod  46704  stoweidlem26  46781  stoweidlem27  46782  stoweidlem31  46786  stoweidlem34  46789  stoweidlem46  46801  fourierdlem79  46940  fourierdlem96  46957  fourierdlem97  46958  fourierdlem98  46959  fourierdlem99  46960  fourierdlem105  46966  fourierdlem107  46968  fourierdlem108  46969  fourierdlem110  46971  etransclem11  47000  salgenval  47076  subsaliuncl  47113  ovnval  47296  ovnval2  47300  ovnval2b  47307  ovncvrrp  47319  ovnsubaddlem1  47325  ovnsubadd  47327  ovncvr2  47366  hspmbl  47384  ovolval2  47399  ovnovollem3  47413  salpreimagelt  47462  salpreimalegt  47464  salpreimagtge  47480  salpreimaltle  47481  issmflem  47482  issmf  47483  salpreimagtlt  47485  smfpreimalt  47486  smfpreimaltf  47491  issmfle  47500  smfpimltxr  47502  smfpreimale  47509  issmfgt  47511  smfpreimagt  47517  issmfge  47525  smflimlem3  47528  smflimlem4  47529  smflim  47532  smfpimgtxr  47535  smfpreimage  47537  fvmptrabdm  48071  elsetpreimafveq  48187  prmdvdsfmtnof1  48380  fppr  48532  dfclnbgr2  48629  dfclnbgr3  48632  dfsclnbgr6  48664  grlimedgclnbgr  48801  grlimgrtri  48809  grilcbri2  48817  bigoval  49370  line  49553  rrxline  49555  sphere  49568  line2y  49576  inpw  49644