Theorem rabbidv 3444

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rab 3437

This theorem is referenced by:  difeq2  4120  seex  5644  mptiniseg  6259  dfpred3g  6333  elovmporab  7679  elovmpt3rab1  7693  naddcllem  8714  naddov2  8717  naddcom  8720  naddrid  8721  naddass  8734  fineqvlem  9298  mapfien2  9449  supeq1  9485  supeq2  9488  supeq3  9489  oieq1  9552  oieq2  9553  ordtypecbv  9557  ordtypelem3  9560  harval  9600  inf3lema  9664  wemapwe  9737  oef1o  9738  tz9.12lem3  9829  rankvalb  9837  rankvalg  9857  ranksnb  9867  rankonidlem  9868  cardval3  9992  cardidm  9999  alephsuc2  10120  coftr  10313  fin1a2lem11  10450  fin1a2lem12  10451  hsmex  10472  axdc3lem2  10491  zorn2lem1  10536  zorn2lem6  10541  zorn2lem7  10542  zorn2g  10543  wuncval  10782  tskmval  10879  peano5uzti  12708  uzval  12880  rpnnen1  13025  ixxval  13395  fzval  13549  hashbclem  14491  hashbc  14492  shftfn  15112  bitsfval  16460  sadfval  16489  sadcom  16500  smufval  16514  smupp1  16517  smupval  16525  smumullem  16529  gcdval  16533  bezoutlem2  16577  bezoutlem4  16579  lcmval  16629  lcmfval  16658  lcmf0val  16659  lcmfpr  16664  isprm  16710  odzval  16829  pcval  16882  pceulem  16883  pceu  16884  pczpre  16885  pcdiv  16890  prmreclem1  16954  prmreclem4  16957  prmreclem5  16958  ramval  17046  cshws0  17139  imasdsval  17560  mrcval  17653  eldmcoa  18110  cycsubg2  19228  cntzval  19339  cntzsnval  19342  odfval  19550  odfvalALT  19551  odval  19552  gexval  19596  efgsfo  19757  dprdval  20023  ablfac1a  20089  ablfac1b  20090  ablfac1eu  20093  ablfaclem1  20105  ablfaclem3  20107  rnghmval  20440  rgspnval  20612  lspval  20973  ocvval  21685  dsmmelbas  21759  frlmsslss  21794  aspval  21893  psrass1lem  21952  psrmulval  21964  mplmonmul  22054  mhpval  22143  mhpmulcl  22153  coe1mul2  22272  pmatcoe1fsupp  22707  istopon  22918  toponsspwpw  22928  clsval  23045  neival  23110  ordtbaslem  23196  ordtbas2  23199  ordtopn1  23202  ordtopn2  23203  cnpval  23244  llyeq  23478  nllyeq  23479  ptfinfin  23527  finlocfin  23528  dissnlocfin  23537  locfindis  23538  xkoopn  23597  kqfval  23731  tsmsfbas  24136  blvalps  24395  blval  24396  nmofval  24735  nmoval  24736  ishtpy  25004  minveclem3b  25462  minveclem3  25463  minveclem4  25466  minveclem5  25467  ovolval  25508  vitalilem2  25644  vitalilem3  25645  vitalilem4  25646  vitali  25648  itg2monolem1  25785  elcpn  25970  mdegmullem  26117  elqaalem1  26361  elqaalem2  26362  elqaalem3  26363  elqaa  26364  aannenlem1  26370  aannenlem2  26371  jensen  27032  vmaval  27156  muval  27175  sgmval  27185  fsumdvdscom  27228  musum  27234  muinv  27236  dchrisum0fval  27549  dchrisum0ff  27551  logsqvma2  27587  pntrlog2bndlem1  27621  scutval  27845  tglngval  28559  ttgval  28883  ttgvalOLD  28884  ttgitvval  28896  ebtwntg  28997  numedglnl  29161  dfnbgr2  29354  dfnbgr3  29355  uvtxusgr  29419  vtxdgval  29486  rusgrnumwrdl2  29604  iswwlksnon  29873  rusgrnumwwlks  29994  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwlknf1oclwwlknlem2  30101  clwwlknon  30109  clwwlk0on0  30111  eupth2  30258  fusgreg2wsplem  30352  fusgreghash2wsp  30357  numclwlk1lem1  30388  sspval  30742  ubthlem1  30889  ubthlem2  30890  ubthlem3  30891  ocval  31299  spanval  31352  chsupid  31431  eigvecval  31915  specval  31917  iunpreima  32577  pwrssmgc  32990  nsgqusf1olem3  33443  minplyval  33748  constrsuc  33779  crefeq  33844  zarcls1  33868  zarclsun  33869  zarclsiin  33870  zarclsint  33871  zarclssn  33872  zartop  33875  zartopon  33876  zart0  33878  zarmxt1  33879  zarcmp  33881  rhmpreimacnlem  33883  rhmpreimacn  33884  ordtcnvNEW  33919  ordtrest2NEW  33922  ordtconnlem1  33923  measvuni  34215  brfae  34249  omsfval  34296  orvcelval  34471  ballotlemi  34503  bnj602  34929  subfacp1lem6  35190  kur14  35221  cvmscbv  35263  cvmsi  35270  cvmsval  35271  snmlval  35336  snmlflim  35337  satfv0  35363  satfv1  35368  satfv0fun  35376  satffunlem1lem1  35407  satffunlem2lem1  35409  satfv0fvfmla0  35418  satfv1fvfmla1  35428  prv1n  35436  fvray  36142  fwddifnval  36164  neibastop3  36363  weiunlem2  36464  icoreval  37354  fin2so  37614  poimirlem26  37653  poimirlem27  37654  poimirlem28  37655  poimirlem32  37659  ftc1anclem6  37705  islinei  39742  pmapval  39759  paddval  39800  paddcom  39815  pclvalN  39892  ldilset  40111  dilsetN  40155  diafval  41033  diaval  41034  docavalN  41125  dicfval  41177  dochfval  41352  dochval  41353  mapdval  41630  mapdsn2  41644  grpods  42195  unitscyglem1  42196  unitscyglem2  42197  unitscyglem3  42198  unitscyglem4  42199  prjcrvval  42642  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  eldioph4i  42823  diophren  42824  pell1qrval  42857  pell14qrval  42859  pell1234qrval  42861  rpnnen3  43044  fnwe2lem1  43062  pwssplit4  43101  pwslnmlem2  43105  dgraaval  43156  itgoval  43173  proot1hash  43207  rp-intrabeq  43233  rp-unirabeq  43234  rfovfvd  44015  rfovfvfvd  44016  rfovcnvf1od  44017  fsovrfovd  44022  fsovfvd  44023  fsovfvfvd  44024  fsovcnvlem  44026  nzss  44336  supminfxr  45475  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  dvnprod  45964  stoweidlem26  46041  stoweidlem27  46042  stoweidlem31  46046  stoweidlem34  46049  stoweidlem46  46061  fourierdlem79  46200  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem105  46226  fourierdlem107  46228  fourierdlem108  46229  fourierdlem110  46231  etransclem11  46260  salgenval  46336  subsaliuncl  46373  ovnval  46556  ovnval2  46560  ovnval2b  46567  ovncvrrp  46579  ovnsubaddlem1  46585  ovnsubadd  46587  ovncvr2  46626  hspmbl  46644  ovolval2  46659  ovnovollem3  46673  salpreimagelt  46722  salpreimalegt  46724  salpreimagtge  46740  salpreimaltle  46741  issmflem  46742  issmf  46743  salpreimagtlt  46745  smfpreimalt  46746  smfpreimaltf  46751  issmfle  46760  smfpimltxr  46762  smfpreimale  46769  issmfgt  46771  smfpreimagt  46777  issmfge  46785  smflimlem3  46788  smflimlem4  46789  smflim  46792  smfpimgtxr  46795  smfpreimage  46797  fvmptrabdm  47305  elsetpreimafveq  47384  prmdvdsfmtnof1  47574  fppr  47713  dfclnbgr2  47810  dfclnbgr3  47813  dfsclnbgr6  47844  grlimgrtri  47963  grilcbri2  47971  bigoval  48470  line  48653  rrxline  48655  sphere  48668  line2y  48676  inpw  48738