Theorem rabbidv 3416

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-rab 3409

This theorem is referenced by:  difeq2  4086  seex  5600  mptiniseg  6215  dfpred3g  6289  elovmporab  7638  elovmpt3rab1  7652  naddcllem  8643  naddov2  8646  naddcom  8649  naddrid  8650  naddass  8663  fineqvlem  9216  mapfien2  9367  supeq1  9403  supeq2  9406  supeq3  9407  oieq1  9472  oieq2  9473  ordtypecbv  9477  ordtypelem3  9480  harval  9520  inf3lema  9584  wemapwe  9657  oef1o  9658  tz9.12lem3  9749  rankvalb  9757  rankvalg  9777  ranksnb  9787  rankonidlem  9788  cardval3  9912  cardidm  9919  alephsuc2  10040  coftr  10233  fin1a2lem11  10370  fin1a2lem12  10371  hsmex  10392  axdc3lem2  10411  zorn2lem1  10456  zorn2lem6  10461  zorn2lem7  10462  zorn2g  10463  wuncval  10702  tskmval  10799  peano5uzti  12631  uzval  12802  rpnnen1  12949  ixxval  13321  fzval  13477  hashbclem  14424  hashbc  14425  shftfn  15046  bitsfval  16400  sadfval  16429  sadcom  16440  smufval  16454  smupp1  16457  smupval  16465  smumullem  16469  gcdval  16473  bezoutlem2  16517  bezoutlem4  16519  lcmval  16569  lcmfval  16598  lcmf0val  16599  lcmfpr  16604  isprm  16650  odzval  16769  pcval  16822  pceulem  16823  pceu  16824  pczpre  16825  pcdiv  16830  prmreclem1  16894  prmreclem4  16897  prmreclem5  16898  ramval  16986  cshws0  17079  imasdsval  17485  mrcval  17578  eldmcoa  18034  cycsubg2  19149  cntzval  19260  cntzsnval  19263  odfval  19469  odfvalALT  19470  odval  19471  gexval  19515  efgsfo  19676  dprdval  19942  ablfac1a  20008  ablfac1b  20009  ablfac1eu  20012  ablfaclem1  20024  ablfaclem3  20026  rnghmval  20356  rgspnval  20528  lspval  20888  ocvval  21583  dsmmelbas  21655  frlmsslss  21690  aspval  21789  psrass1lem  21848  psrmulval  21860  mplmonmul  21950  mhpval  22033  mhpmulcl  22043  coe1mul2  22162  pmatcoe1fsupp  22595  istopon  22806  toponsspwpw  22816  clsval  22931  neival  22996  ordtbaslem  23082  ordtbas2  23085  ordtopn1  23088  ordtopn2  23089  cnpval  23130  llyeq  23364  nllyeq  23365  ptfinfin  23413  finlocfin  23414  dissnlocfin  23423  locfindis  23424  xkoopn  23483  kqfval  23617  tsmsfbas  24022  blvalps  24280  blval  24281  nmofval  24609  nmoval  24610  ishtpy  24878  minveclem3b  25335  minveclem3  25336  minveclem4  25339  minveclem5  25340  ovolval  25381  vitalilem2  25517  vitalilem3  25518  vitalilem4  25519  vitali  25521  itg2monolem1  25658  elcpn  25843  mdegmullem  25990  elqaalem1  26234  elqaalem2  26235  elqaalem3  26236  elqaa  26237  aannenlem1  26243  aannenlem2  26244  jensen  26906  vmaval  27030  muval  27049  sgmval  27059  fsumdvdscom  27102  musum  27108  muinv  27110  dchrisum0fval  27423  dchrisum0ff  27425  logsqvma2  27461  pntrlog2bndlem1  27495  scutval  27719  bdayon  28180  tglngval  28485  ttgval  28809  ttgitvval  28816  ebtwntg  28916  numedglnl  29078  dfnbgr2  29271  dfnbgr3  29272  uvtxusgr  29336  vtxdgval  29403  rusgrnumwrdl2  29521  iswwlksnon  29790  rusgrnumwwlks  29911  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwlknf1oclwwlknlem2  30018  clwwlknon  30026  clwwlk0on0  30028  eupth2  30175  fusgreg2wsplem  30269  fusgreghash2wsp  30274  numclwlk1lem1  30305  sspval  30659  ubthlem1  30806  ubthlem2  30807  ubthlem3  30808  ocval  31216  spanval  31269  chsupid  31348  eigvecval  31832  specval  31834  iunpreima  32500  pwrssmgc  32933  fxpgaval  33131  nsgqusf1olem3  33393  minplyval  33702  constrsuc  33735  constrcbvlem  33752  crefeq  33842  zarcls1  33866  zarclsun  33867  zarclsiin  33868  zarclsint  33869  zarclssn  33870  zartop  33873  zartopon  33874  zart0  33876  zarmxt1  33877  zarcmp  33879  rhmpreimacnlem  33881  rhmpreimacn  33882  ordtcnvNEW  33917  ordtrest2NEW  33920  ordtconnlem1  33921  measvuni  34211  brfae  34245  omsfval  34292  orvcelval  34467  ballotlemi  34499  bnj602  34912  onvf1odlem3  35099  subfacp1lem6  35179  kur14  35210  cvmscbv  35252  cvmsi  35259  cvmsval  35260  snmlval  35325  snmlflim  35326  satfv0  35352  satfv1  35357  satfv0fun  35365  satffunlem1lem1  35396  satffunlem2lem1  35398  satfv0fvfmla0  35407  satfv1fvfmla1  35417  prv1n  35425  fvray  36136  fwddifnval  36158  neibastop3  36357  weiunlem2  36458  icoreval  37348  fin2so  37608  poimirlem26  37647  poimirlem27  37648  poimirlem28  37649  poimirlem32  37653  ftc1anclem6  37699  islinei  39741  pmapval  39758  paddval  39799  paddcom  39814  pclvalN  39891  ldilset  40110  dilsetN  40154  diafval  41032  diaval  41033  docavalN  41124  dicfval  41176  dochfval  41351  dochval  41352  mapdval  41629  mapdsn2  41643  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem3  42192  unitscyglem4  42193  prjcrvval  42627  2rexfrabdioph  42791  3rexfrabdioph  42792  4rexfrabdioph  42793  6rexfrabdioph  42794  7rexfrabdioph  42795  eldioph4i  42807  diophren  42808  pell1qrval  42841  pell14qrval  42843  pell1234qrval  42845  rpnnen3  43028  fnwe2lem1  43046  pwssplit4  43085  pwslnmlem2  43089  dgraaval  43140  itgoval  43157  proot1hash  43191  rp-intrabeq  43217  rp-unirabeq  43218  rfovfvd  43998  rfovfvfvd  43999  rfovcnvf1od  44000  fsovrfovd  44005  fsovfvd  44006  fsovfvfvd  44007  fsovcnvlem  44009  nzss  44313  supminfxr  45467  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  dvnprod  45954  stoweidlem26  46031  stoweidlem27  46032  stoweidlem31  46036  stoweidlem34  46039  stoweidlem46  46051  fourierdlem79  46190  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem105  46216  fourierdlem107  46218  fourierdlem108  46219  fourierdlem110  46221  etransclem11  46250  salgenval  46326  subsaliuncl  46363  ovnval  46546  ovnval2  46550  ovnval2b  46557  ovncvrrp  46569  ovnsubaddlem1  46575  ovnsubadd  46577  ovncvr2  46616  hspmbl  46634  ovolval2  46649  ovnovollem3  46663  salpreimagelt  46712  salpreimalegt  46714  salpreimagtge  46730  salpreimaltle  46731  issmflem  46732  issmf  46733  salpreimagtlt  46735  smfpreimalt  46736  smfpreimaltf  46741  issmfle  46750  smfpimltxr  46752  smfpreimale  46759  issmfgt  46761  smfpreimagt  46767  issmfge  46775  smflimlem3  46778  smflimlem4  46779  smflim  46782  smfpimgtxr  46785  smfpreimage  46787  fvmptrabdm  47298  elsetpreimafveq  47402  prmdvdsfmtnof1  47592  fppr  47731  dfclnbgr2  47828  dfclnbgr3  47831  dfsclnbgr6  47862  grlimgrtri  47999  grilcbri2  48007  bigoval  48542  line  48725  rrxline  48727  sphere  48740  line2y  48748  inpw  48817