Theorem rabbidv 3406

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400

This theorem is referenced by:  difeq2  4072  seex  5583  mptiniseg  6197  dfpred3g  6271  elovmporab  7604  elovmpt3rab1  7618  naddcllem  8604  naddov2  8607  naddcom  8610  naddrid  8611  naddass  8624  fineqvlem  9166  mapfien2  9312  supeq1  9348  supeq2  9351  supeq3  9352  oieq1  9417  oieq2  9418  ordtypecbv  9422  ordtypelem3  9425  harval  9465  inf3lema  9533  wemapwe  9606  oef1o  9607  tz9.12lem3  9701  rankvalb  9709  rankvalg  9729  ranksnb  9739  rankonidlem  9740  cardval3  9864  cardidm  9871  alephsuc2  9990  coftr  10183  fin1a2lem11  10320  fin1a2lem12  10321  hsmex  10342  axdc3lem2  10361  zorn2lem1  10406  zorn2lem6  10411  zorn2lem7  10412  zorn2g  10413  wuncval  10653  tskmval  10750  peano5uzti  12582  uzval  12753  rpnnen1  12896  ixxval  13269  fzval  13425  hashbclem  14375  hashbc  14376  shftfn  14996  bitsfval  16350  sadfval  16379  sadcom  16390  smufval  16404  smupp1  16407  smupval  16415  smumullem  16419  gcdval  16423  bezoutlem2  16467  bezoutlem4  16469  lcmval  16519  lcmfval  16548  lcmf0val  16549  lcmfpr  16554  isprm  16600  odzval  16719  pcval  16772  pceulem  16773  pceu  16774  pczpre  16775  pcdiv  16780  prmreclem1  16844  prmreclem4  16847  prmreclem5  16848  ramval  16936  cshws0  17029  imasdsval  17436  mrcval  17533  eldmcoa  17989  chneq1  18535  cycsubg2  19139  cntzval  19250  cntzsnval  19253  odfval  19461  odfvalALT  19462  odval  19463  gexval  19507  efgsfo  19668  dprdval  19934  ablfac1a  20000  ablfac1b  20001  ablfac1eu  20004  ablfaclem1  20016  ablfaclem3  20018  rnghmval  20376  rgspnval  20545  lspval  20926  ocvval  21622  dsmmelbas  21694  frlmsslss  21729  aspval  21828  psrass1lem  21888  psrmulval  21900  mplmonmul  21991  mhpval  22082  mhpmulcl  22092  coe1mul2  22211  pmatcoe1fsupp  22645  istopon  22856  toponsspwpw  22866  clsval  22981  neival  23046  ordtbaslem  23132  ordtbas2  23135  ordtopn1  23138  ordtopn2  23139  cnpval  23180  llyeq  23414  nllyeq  23415  ptfinfin  23463  finlocfin  23464  dissnlocfin  23473  locfindis  23474  xkoopn  23533  kqfval  23667  tsmsfbas  24072  blvalps  24329  blval  24330  nmofval  24658  nmoval  24659  ishtpy  24927  minveclem3b  25384  minveclem3  25385  minveclem4  25388  minveclem5  25389  ovolval  25430  vitalilem2  25566  vitalilem3  25567  vitalilem4  25568  vitali  25570  itg2monolem1  25707  elcpn  25892  mdegmullem  26039  elqaalem1  26283  elqaalem2  26284  elqaalem3  26285  elqaa  26286  aannenlem1  26292  aannenlem2  26293  jensen  26955  vmaval  27079  muval  27098  sgmval  27108  fsumdvdscom  27151  musum  27157  muinv  27159  dchrisum0fval  27472  dchrisum0ff  27474  logsqvma2  27510  pntrlog2bndlem1  27544  cutsval  27776  bdayons  28272  tglngval  28623  ttgval  28947  ttgitvval  28954  ebtwntg  29055  numedglnl  29217  dfnbgr2  29410  dfnbgr3  29411  uvtxusgr  29475  vtxdgval  29542  rusgrnumwrdl2  29660  iswwlksnon  29926  rusgrnumwwlks  30050  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwlknf1oclwwlknlem2  30157  clwwlknon  30165  clwwlk0on0  30167  eupth2  30314  fusgreg2wsplem  30408  fusgreghash2wsp  30413  numclwlk1lem1  30444  sspval  30798  ubthlem1  30945  ubthlem2  30946  ubthlem3  30947  ocval  31355  spanval  31408  chsupid  31487  eigvecval  31971  specval  31973  iunpreima  32639  fcobijfs2  32801  pwrssmgc  33082  fxpgaval  33249  nsgqusf1olem3  33496  mplvrpmrhm  33712  esplyfval  33721  esplyfval0  33722  minplyval  33862  constrsuc  33895  constrcbvlem  33912  crefeq  34002  zarcls1  34026  zarclsun  34027  zarclsiin  34028  zarclsint  34029  zarclssn  34030  zartop  34033  zartopon  34034  zart0  34036  zarmxt1  34037  zarcmp  34039  rhmpreimacnlem  34041  rhmpreimacn  34042  ordtcnvNEW  34077  ordtrest2NEW  34080  ordtconnlem1  34081  measvuni  34371  brfae  34405  omsfval  34451  orvcelval  34626  ballotlemi  34658  bnj602  35071  fineqvnttrclselem2  35278  fineqvnttrclselem3  35279  fineqvnttrclse  35280  onvf1odlem3  35299  subfacp1lem6  35379  kur14  35410  cvmscbv  35452  cvmsi  35459  cvmsval  35460  snmlval  35525  snmlflim  35526  satfv0  35552  satfv1  35557  satfv0fun  35565  satffunlem1lem1  35596  satffunlem2lem1  35598  satfv0fvfmla0  35607  satfv1fvfmla1  35617  prv1n  35625  fvray  36335  fwddifnval  36357  neibastop3  36556  weiunlem  36657  icoreval  37554  fin2so  37804  poimirlem26  37843  poimirlem27  37844  poimirlem28  37845  poimirlem32  37849  ftc1anclem6  37895  islinei  39996  pmapval  40013  paddval  40054  paddcom  40069  pclvalN  40146  ldilset  40365  dilsetN  40409  diafval  41287  diaval  41288  docavalN  41379  dicfval  41431  dochfval  41606  dochval  41607  mapdval  41884  mapdsn2  41898  grpods  42444  unitscyglem1  42445  unitscyglem2  42446  unitscyglem3  42447  unitscyglem4  42448  prjcrvval  42871  2rexfrabdioph  43034  3rexfrabdioph  43035  4rexfrabdioph  43036  6rexfrabdioph  43037  7rexfrabdioph  43038  eldioph4i  43050  diophren  43051  pell1qrval  43084  pell14qrval  43086  pell1234qrval  43088  rpnnen3  43270  fnwe2lem1  43288  pwssplit4  43327  pwslnmlem2  43331  dgraaval  43382  itgoval  43399  proot1hash  43433  rp-intrabeq  43459  rp-unirabeq  43460  rfovfvd  44239  rfovfvfvd  44240  rfovcnvf1od  44241  fsovrfovd  44246  fsovfvd  44247  fsovfvfvd  44248  fsovcnvlem  44250  nzss  44554  supminfxr  45704  dvnprodlem1  46186  dvnprodlem2  46187  dvnprodlem3  46188  dvnprod  46189  stoweidlem26  46266  stoweidlem27  46267  stoweidlem31  46271  stoweidlem34  46274  stoweidlem46  46286  fourierdlem79  46425  fourierdlem96  46442  fourierdlem97  46443  fourierdlem98  46444  fourierdlem99  46445  fourierdlem105  46451  fourierdlem107  46453  fourierdlem108  46454  fourierdlem110  46456  etransclem11  46485  salgenval  46561  subsaliuncl  46598  ovnval  46781  ovnval2  46785  ovnval2b  46792  ovncvrrp  46804  ovnsubaddlem1  46810  ovnsubadd  46812  ovncvr2  46851  hspmbl  46869  ovolval2  46884  ovnovollem3  46898  salpreimagelt  46947  salpreimalegt  46949  salpreimagtge  46965  salpreimaltle  46966  issmflem  46967  issmf  46968  salpreimagtlt  46970  smfpreimalt  46971  smfpreimaltf  46976  issmfle  46985  smfpimltxr  46987  smfpreimale  46994  issmfgt  46996  smfpreimagt  47002  issmfge  47010  smflimlem3  47013  smflimlem4  47014  smflim  47017  smfpimgtxr  47020  smfpreimage  47022  fvmptrabdm  47535  elsetpreimafveq  47639  prmdvdsfmtnof1  47829  fppr  47968  dfclnbgr2  48065  dfclnbgr3  48068  dfsclnbgr6  48100  grlimedgclnbgr  48237  grlimgrtri  48245  grilcbri2  48253  bigoval  48791  line  48974  rrxline  48976  sphere  48989  line2y  48997  inpw  49066