Theorem rabbidv 3413

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3406

This theorem is referenced by:  difeq2  4083  seex  5597  mptiniseg  6212  dfpred3g  6286  elovmporab  7635  elovmpt3rab1  7649  naddcllem  8640  naddov2  8643  naddcom  8646  naddrid  8647  naddass  8660  fineqvlem  9209  mapfien2  9360  supeq1  9396  supeq2  9399  supeq3  9400  oieq1  9465  oieq2  9466  ordtypecbv  9470  ordtypelem3  9473  harval  9513  inf3lema  9577  wemapwe  9650  oef1o  9651  tz9.12lem3  9742  rankvalb  9750  rankvalg  9770  ranksnb  9780  rankonidlem  9781  cardval3  9905  cardidm  9912  alephsuc2  10033  coftr  10226  fin1a2lem11  10363  fin1a2lem12  10364  hsmex  10385  axdc3lem2  10404  zorn2lem1  10449  zorn2lem6  10454  zorn2lem7  10455  zorn2g  10456  wuncval  10695  tskmval  10792  peano5uzti  12624  uzval  12795  rpnnen1  12942  ixxval  13314  fzval  13470  hashbclem  14417  hashbc  14418  shftfn  15039  bitsfval  16393  sadfval  16422  sadcom  16433  smufval  16447  smupp1  16450  smupval  16458  smumullem  16462  gcdval  16466  bezoutlem2  16510  bezoutlem4  16512  lcmval  16562  lcmfval  16591  lcmf0val  16592  lcmfpr  16597  isprm  16643  odzval  16762  pcval  16815  pceulem  16816  pceu  16817  pczpre  16818  pcdiv  16823  prmreclem1  16887  prmreclem4  16890  prmreclem5  16891  ramval  16979  cshws0  17072  imasdsval  17478  mrcval  17571  eldmcoa  18027  cycsubg2  19142  cntzval  19253  cntzsnval  19256  odfval  19462  odfvalALT  19463  odval  19464  gexval  19508  efgsfo  19669  dprdval  19935  ablfac1a  20001  ablfac1b  20002  ablfac1eu  20005  ablfaclem1  20017  ablfaclem3  20019  rnghmval  20349  rgspnval  20521  lspval  20881  ocvval  21576  dsmmelbas  21648  frlmsslss  21683  aspval  21782  psrass1lem  21841  psrmulval  21853  mplmonmul  21943  mhpval  22026  mhpmulcl  22036  coe1mul2  22155  pmatcoe1fsupp  22588  istopon  22799  toponsspwpw  22809  clsval  22924  neival  22989  ordtbaslem  23075  ordtbas2  23078  ordtopn1  23081  ordtopn2  23082  cnpval  23123  llyeq  23357  nllyeq  23358  ptfinfin  23406  finlocfin  23407  dissnlocfin  23416  locfindis  23417  xkoopn  23476  kqfval  23610  tsmsfbas  24015  blvalps  24273  blval  24274  nmofval  24602  nmoval  24603  ishtpy  24871  minveclem3b  25328  minveclem3  25329  minveclem4  25332  minveclem5  25333  ovolval  25374  vitalilem2  25510  vitalilem3  25511  vitalilem4  25512  vitali  25514  itg2monolem1  25651  elcpn  25836  mdegmullem  25983  elqaalem1  26227  elqaalem2  26228  elqaalem3  26229  elqaa  26230  aannenlem1  26236  aannenlem2  26237  jensen  26899  vmaval  27023  muval  27042  sgmval  27052  fsumdvdscom  27095  musum  27101  muinv  27103  dchrisum0fval  27416  dchrisum0ff  27418  logsqvma2  27454  pntrlog2bndlem1  27488  scutval  27712  bdayon  28173  tglngval  28478  ttgval  28802  ttgitvval  28809  ebtwntg  28909  numedglnl  29071  dfnbgr2  29264  dfnbgr3  29265  uvtxusgr  29329  vtxdgval  29396  rusgrnumwrdl2  29514  iswwlksnon  29783  rusgrnumwwlks  29904  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwlknf1oclwwlknlem2  30011  clwwlknon  30019  clwwlk0on0  30021  eupth2  30168  fusgreg2wsplem  30262  fusgreghash2wsp  30267  numclwlk1lem1  30298  sspval  30652  ubthlem1  30799  ubthlem2  30800  ubthlem3  30801  ocval  31209  spanval  31262  chsupid  31341  eigvecval  31825  specval  31827  iunpreima  32493  pwrssmgc  32926  fxpgaval  33124  nsgqusf1olem3  33386  minplyval  33695  constrsuc  33728  constrcbvlem  33745  crefeq  33835  zarcls1  33859  zarclsun  33860  zarclsiin  33861  zarclsint  33862  zarclssn  33863  zartop  33866  zartopon  33867  zart0  33869  zarmxt1  33870  zarcmp  33872  rhmpreimacnlem  33874  rhmpreimacn  33875  ordtcnvNEW  33910  ordtrest2NEW  33913  ordtconnlem1  33914  measvuni  34204  brfae  34238  omsfval  34285  orvcelval  34460  ballotlemi  34492  bnj602  34905  onvf1odlem3  35092  subfacp1lem6  35172  kur14  35203  cvmscbv  35245  cvmsi  35252  cvmsval  35253  snmlval  35318  snmlflim  35319  satfv0  35345  satfv1  35350  satfv0fun  35358  satffunlem1lem1  35389  satffunlem2lem1  35391  satfv0fvfmla0  35400  satfv1fvfmla1  35410  prv1n  35418  fvray  36129  fwddifnval  36151  neibastop3  36350  weiunlem2  36451  icoreval  37341  fin2so  37601  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem32  37646  ftc1anclem6  37692  islinei  39734  pmapval  39751  paddval  39792  paddcom  39807  pclvalN  39884  ldilset  40103  dilsetN  40147  diafval  41025  diaval  41026  docavalN  41117  dicfval  41169  dochfval  41344  dochval  41345  mapdval  41622  mapdsn2  41636  grpods  42182  unitscyglem1  42183  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  prjcrvval  42620  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  eldioph4i  42800  diophren  42801  pell1qrval  42834  pell14qrval  42836  pell1234qrval  42838  rpnnen3  43021  fnwe2lem1  43039  pwssplit4  43078  pwslnmlem2  43082  dgraaval  43133  itgoval  43150  proot1hash  43184  rp-intrabeq  43210  rp-unirabeq  43211  rfovfvd  43991  rfovfvfvd  43992  rfovcnvf1od  43993  fsovrfovd  43998  fsovfvd  43999  fsovfvfvd  44000  fsovcnvlem  44002  nzss  44306  supminfxr  45460  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  stoweidlem26  46024  stoweidlem27  46025  stoweidlem31  46029  stoweidlem34  46032  stoweidlem46  46044  fourierdlem79  46183  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem105  46209  fourierdlem107  46211  fourierdlem108  46212  fourierdlem110  46214  etransclem11  46243  salgenval  46319  subsaliuncl  46356  ovnval  46539  ovnval2  46543  ovnval2b  46550  ovncvrrp  46562  ovnsubaddlem1  46568  ovnsubadd  46570  ovncvr2  46609  hspmbl  46627  ovolval2  46642  ovnovollem3  46656  salpreimagelt  46705  salpreimalegt  46707  salpreimagtge  46723  salpreimaltle  46724  issmflem  46725  issmf  46726  salpreimagtlt  46728  smfpreimalt  46729  smfpreimaltf  46734  issmfle  46743  smfpimltxr  46745  smfpreimale  46752  issmfgt  46754  smfpreimagt  46760  issmfge  46768  smflimlem3  46771  smflimlem4  46772  smflim  46775  smfpimgtxr  46778  smfpreimage  46780  fvmptrabdm  47294  elsetpreimafveq  47398  prmdvdsfmtnof1  47588  fppr  47727  dfclnbgr2  47824  dfclnbgr3  47827  dfsclnbgr6  47858  grlimgrtri  47995  grilcbri2  48003  bigoval  48538  line  48721  rrxline  48723  sphere  48736  line2y  48744  inpw  48813