Theorem rabbidv 3428

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-rab 3421

This theorem is referenced by:  difeq2  4100  seex  5618  mptiniseg  6233  dfpred3g  6307  elovmporab  7658  elovmpt3rab1  7672  naddcllem  8693  naddov2  8696  naddcom  8699  naddrid  8700  naddass  8713  fineqvlem  9275  mapfien2  9426  supeq1  9462  supeq2  9465  supeq3  9466  oieq1  9531  oieq2  9532  ordtypecbv  9536  ordtypelem3  9539  harval  9579  inf3lema  9643  wemapwe  9716  oef1o  9717  tz9.12lem3  9808  rankvalb  9816  rankvalg  9836  ranksnb  9846  rankonidlem  9847  cardval3  9971  cardidm  9978  alephsuc2  10099  coftr  10292  fin1a2lem11  10429  fin1a2lem12  10430  hsmex  10451  axdc3lem2  10470  zorn2lem1  10515  zorn2lem6  10520  zorn2lem7  10521  zorn2g  10522  wuncval  10761  tskmval  10858  peano5uzti  12688  uzval  12859  rpnnen1  13004  ixxval  13375  fzval  13531  hashbclem  14475  hashbc  14476  shftfn  15097  bitsfval  16447  sadfval  16476  sadcom  16487  smufval  16501  smupp1  16504  smupval  16512  smumullem  16516  gcdval  16520  bezoutlem2  16564  bezoutlem4  16566  lcmval  16616  lcmfval  16645  lcmf0val  16646  lcmfpr  16651  isprm  16697  odzval  16816  pcval  16869  pceulem  16870  pceu  16871  pczpre  16872  pcdiv  16877  prmreclem1  16941  prmreclem4  16944  prmreclem5  16945  ramval  17033  cshws0  17126  imasdsval  17534  mrcval  17627  eldmcoa  18083  cycsubg2  19198  cntzval  19309  cntzsnval  19312  odfval  19518  odfvalALT  19519  odval  19520  gexval  19564  efgsfo  19725  dprdval  19991  ablfac1a  20057  ablfac1b  20058  ablfac1eu  20061  ablfaclem1  20073  ablfaclem3  20075  rnghmval  20405  rgspnval  20577  lspval  20937  ocvval  21632  dsmmelbas  21704  frlmsslss  21739  aspval  21838  psrass1lem  21897  psrmulval  21909  mplmonmul  21999  mhpval  22082  mhpmulcl  22092  coe1mul2  22211  pmatcoe1fsupp  22644  istopon  22855  toponsspwpw  22865  clsval  22980  neival  23045  ordtbaslem  23131  ordtbas2  23134  ordtopn1  23137  ordtopn2  23138  cnpval  23179  llyeq  23413  nllyeq  23414  ptfinfin  23462  finlocfin  23463  dissnlocfin  23472  locfindis  23473  xkoopn  23532  kqfval  23666  tsmsfbas  24071  blvalps  24329  blval  24330  nmofval  24658  nmoval  24659  ishtpy  24927  minveclem3b  25385  minveclem3  25386  minveclem4  25389  minveclem5  25390  ovolval  25431  vitalilem2  25567  vitalilem3  25568  vitalilem4  25569  vitali  25571  itg2monolem1  25708  elcpn  25893  mdegmullem  26040  elqaalem1  26284  elqaalem2  26285  elqaalem3  26286  elqaa  26287  aannenlem1  26293  aannenlem2  26294  jensen  26956  vmaval  27080  muval  27099  sgmval  27109  fsumdvdscom  27152  musum  27158  muinv  27160  dchrisum0fval  27473  dchrisum0ff  27475  logsqvma2  27511  pntrlog2bndlem1  27545  scutval  27769  bdayon  28230  tglngval  28535  ttgval  28859  ttgitvval  28866  ebtwntg  28966  numedglnl  29128  dfnbgr2  29321  dfnbgr3  29322  uvtxusgr  29386  vtxdgval  29453  rusgrnumwrdl2  29571  iswwlksnon  29840  rusgrnumwwlks  29961  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  clwlknf1oclwwlknlem2  30068  clwwlknon  30076  clwwlk0on0  30078  eupth2  30225  fusgreg2wsplem  30319  fusgreghash2wsp  30324  numclwlk1lem1  30355  sspval  30709  ubthlem1  30856  ubthlem2  30857  ubthlem3  30858  ocval  31266  spanval  31319  chsupid  31398  eigvecval  31882  specval  31884  iunpreima  32550  pwrssmgc  32985  nsgqusf1olem3  33435  minplyval  33744  constrsuc  33777  constrcbvlem  33794  crefeq  33881  zarcls1  33905  zarclsun  33906  zarclsiin  33907  zarclsint  33908  zarclssn  33909  zartop  33912  zartopon  33913  zart0  33915  zarmxt1  33916  zarcmp  33918  rhmpreimacnlem  33920  rhmpreimacn  33921  ordtcnvNEW  33956  ordtrest2NEW  33959  ordtconnlem1  33960  measvuni  34250  brfae  34284  omsfval  34331  orvcelval  34506  ballotlemi  34538  bnj602  34951  subfacp1lem6  35212  kur14  35243  cvmscbv  35285  cvmsi  35292  cvmsval  35293  snmlval  35358  snmlflim  35359  satfv0  35385  satfv1  35390  satfv0fun  35398  satffunlem1lem1  35429  satffunlem2lem1  35431  satfv0fvfmla0  35440  satfv1fvfmla1  35450  prv1n  35458  fvray  36164  fwddifnval  36186  neibastop3  36385  weiunlem2  36486  icoreval  37376  fin2so  37636  poimirlem26  37675  poimirlem27  37676  poimirlem28  37677  poimirlem32  37681  ftc1anclem6  37727  islinei  39764  pmapval  39781  paddval  39822  paddcom  39837  pclvalN  39914  ldilset  40133  dilsetN  40177  diafval  41055  diaval  41056  docavalN  41147  dicfval  41199  dochfval  41374  dochval  41375  mapdval  41652  mapdsn2  41666  grpods  42212  unitscyglem1  42213  unitscyglem2  42214  unitscyglem3  42215  unitscyglem4  42216  prjcrvval  42630  2rexfrabdioph  42794  3rexfrabdioph  42795  4rexfrabdioph  42796  6rexfrabdioph  42797  7rexfrabdioph  42798  eldioph4i  42810  diophren  42811  pell1qrval  42844  pell14qrval  42846  pell1234qrval  42848  rpnnen3  43031  fnwe2lem1  43049  pwssplit4  43088  pwslnmlem2  43092  dgraaval  43143  itgoval  43160  proot1hash  43194  rp-intrabeq  43220  rp-unirabeq  43221  rfovfvd  44001  rfovfvfvd  44002  rfovcnvf1od  44003  fsovrfovd  44008  fsovfvd  44009  fsovfvfvd  44010  fsovcnvlem  44012  nzss  44316  supminfxr  45471  dvnprodlem1  45955  dvnprodlem2  45956  dvnprodlem3  45957  dvnprod  45958  stoweidlem26  46035  stoweidlem27  46036  stoweidlem31  46040  stoweidlem34  46043  stoweidlem46  46055  fourierdlem79  46194  fourierdlem96  46211  fourierdlem97  46212  fourierdlem98  46213  fourierdlem99  46214  fourierdlem105  46220  fourierdlem107  46222  fourierdlem108  46223  fourierdlem110  46225  etransclem11  46254  salgenval  46330  subsaliuncl  46367  ovnval  46550  ovnval2  46554  ovnval2b  46561  ovncvrrp  46573  ovnsubaddlem1  46579  ovnsubadd  46581  ovncvr2  46620  hspmbl  46638  ovolval2  46653  ovnovollem3  46667  salpreimagelt  46716  salpreimalegt  46718  salpreimagtge  46734  salpreimaltle  46735  issmflem  46736  issmf  46737  salpreimagtlt  46739  smfpreimalt  46740  smfpreimaltf  46745  issmfle  46754  smfpimltxr  46756  smfpreimale  46763  issmfgt  46765  smfpreimagt  46771  issmfge  46779  smflimlem3  46782  smflimlem4  46783  smflim  46786  smfpimgtxr  46789  smfpreimage  46791  fvmptrabdm  47302  elsetpreimafveq  47391  prmdvdsfmtnof1  47581  fppr  47720  dfclnbgr2  47817  dfclnbgr3  47820  dfsclnbgr6  47851  grlimgrtri  47988  grilcbri2  47996  bigoval  48509  line  48692  rrxline  48694  sphere  48707  line2y  48715  inpw  48783