Theorem rabbidv 3404

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

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

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 3397

This theorem is referenced by:  difeq2  4073  seex  5582  mptiniseg  6192  dfpred3g  6265  elovmporab  7599  elovmpt3rab1  7613  naddcllem  8601  naddov2  8604  naddcom  8607  naddrid  8608  naddass  8621  fineqvlem  9167  mapfien2  9318  supeq1  9354  supeq2  9357  supeq3  9358  oieq1  9423  oieq2  9424  ordtypecbv  9428  ordtypelem3  9431  harval  9471  inf3lema  9539  wemapwe  9612  oef1o  9613  tz9.12lem3  9704  rankvalb  9712  rankvalg  9732  ranksnb  9742  rankonidlem  9743  cardval3  9867  cardidm  9874  alephsuc2  9993  coftr  10186  fin1a2lem11  10323  fin1a2lem12  10324  hsmex  10345  axdc3lem2  10364  zorn2lem1  10409  zorn2lem6  10414  zorn2lem7  10415  zorn2g  10416  wuncval  10655  tskmval  10752  peano5uzti  12584  uzval  12755  rpnnen1  12902  ixxval  13274  fzval  13430  hashbclem  14377  hashbc  14378  shftfn  14998  bitsfval  16352  sadfval  16381  sadcom  16392  smufval  16406  smupp1  16409  smupval  16417  smumullem  16421  gcdval  16425  bezoutlem2  16469  bezoutlem4  16471  lcmval  16521  lcmfval  16550  lcmf0val  16551  lcmfpr  16556  isprm  16602  odzval  16721  pcval  16774  pceulem  16775  pceu  16776  pczpre  16777  pcdiv  16782  prmreclem1  16846  prmreclem4  16849  prmreclem5  16850  ramval  16938  cshws0  17031  imasdsval  17437  mrcval  17534  eldmcoa  17990  cycsubg2  19107  cntzval  19218  cntzsnval  19221  odfval  19429  odfvalALT  19430  odval  19431  gexval  19475  efgsfo  19636  dprdval  19902  ablfac1a  19968  ablfac1b  19969  ablfac1eu  19972  ablfaclem1  19984  ablfaclem3  19986  rnghmval  20343  rgspnval  20515  lspval  20896  ocvval  21592  dsmmelbas  21664  frlmsslss  21699  aspval  21798  psrass1lem  21857  psrmulval  21869  mplmonmul  21959  mhpval  22042  mhpmulcl  22052  coe1mul2  22171  pmatcoe1fsupp  22604  istopon  22815  toponsspwpw  22825  clsval  22940  neival  23005  ordtbaslem  23091  ordtbas2  23094  ordtopn1  23097  ordtopn2  23098  cnpval  23139  llyeq  23373  nllyeq  23374  ptfinfin  23422  finlocfin  23423  dissnlocfin  23432  locfindis  23433  xkoopn  23492  kqfval  23626  tsmsfbas  24031  blvalps  24289  blval  24290  nmofval  24618  nmoval  24619  ishtpy  24887  minveclem3b  25344  minveclem3  25345  minveclem4  25348  minveclem5  25349  ovolval  25390  vitalilem2  25526  vitalilem3  25527  vitalilem4  25528  vitali  25530  itg2monolem1  25667  elcpn  25852  mdegmullem  25999  elqaalem1  26243  elqaalem2  26244  elqaalem3  26245  elqaa  26246  aannenlem1  26252  aannenlem2  26253  jensen  26915  vmaval  27039  muval  27058  sgmval  27068  fsumdvdscom  27111  musum  27117  muinv  27119  dchrisum0fval  27432  dchrisum0ff  27434  logsqvma2  27470  pntrlog2bndlem1  27504  scutval  27729  bdayon  28196  tglngval  28514  ttgval  28838  ttgitvval  28845  ebtwntg  28945  numedglnl  29107  dfnbgr2  29300  dfnbgr3  29301  uvtxusgr  29365  vtxdgval  29432  rusgrnumwrdl2  29550  iswwlksnon  29816  rusgrnumwwlks  29937  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  clwlknf1oclwwlknlem2  30044  clwwlknon  30052  clwwlk0on0  30054  eupth2  30201  fusgreg2wsplem  30295  fusgreghash2wsp  30300  numclwlk1lem1  30331  sspval  30685  ubthlem1  30832  ubthlem2  30833  ubthlem3  30834  ocval  31242  spanval  31295  chsupid  31374  eigvecval  31858  specval  31860  iunpreima  32526  pwrssmgc  32955  fxpgaval  33122  nsgqusf1olem3  33362  minplyval  33671  constrsuc  33704  constrcbvlem  33721  crefeq  33811  zarcls1  33835  zarclsun  33836  zarclsiin  33837  zarclsint  33838  zarclssn  33839  zartop  33842  zartopon  33843  zart0  33845  zarmxt1  33846  zarcmp  33848  rhmpreimacnlem  33850  rhmpreimacn  33851  ordtcnvNEW  33886  ordtrest2NEW  33889  ordtconnlem1  33890  measvuni  34180  brfae  34214  omsfval  34261  orvcelval  34436  ballotlemi  34468  bnj602  34881  onvf1odlem3  35077  subfacp1lem6  35157  kur14  35188  cvmscbv  35230  cvmsi  35237  cvmsval  35238  snmlval  35303  snmlflim  35304  satfv0  35330  satfv1  35335  satfv0fun  35343  satffunlem1lem1  35374  satffunlem2lem1  35376  satfv0fvfmla0  35385  satfv1fvfmla1  35395  prv1n  35403  fvray  36114  fwddifnval  36136  neibastop3  36335  weiunlem2  36436  icoreval  37326  fin2so  37586  poimirlem26  37625  poimirlem27  37626  poimirlem28  37627  poimirlem32  37631  ftc1anclem6  37677  islinei  39719  pmapval  39736  paddval  39777  paddcom  39792  pclvalN  39869  ldilset  40088  dilsetN  40132  diafval  41010  diaval  41011  docavalN  41102  dicfval  41154  dochfval  41329  dochval  41330  mapdval  41607  mapdsn2  41621  grpods  42167  unitscyglem1  42168  unitscyglem2  42169  unitscyglem3  42170  unitscyglem4  42171  prjcrvval  42605  2rexfrabdioph  42769  3rexfrabdioph  42770  4rexfrabdioph  42771  6rexfrabdioph  42772  7rexfrabdioph  42773  eldioph4i  42785  diophren  42786  pell1qrval  42819  pell14qrval  42821  pell1234qrval  42823  rpnnen3  43005  fnwe2lem1  43023  pwssplit4  43062  pwslnmlem2  43066  dgraaval  43117  itgoval  43134  proot1hash  43168  rp-intrabeq  43194  rp-unirabeq  43195  rfovfvd  43975  rfovfvfvd  43976  rfovcnvf1od  43977  fsovrfovd  43982  fsovfvd  43983  fsovfvfvd  43984  fsovcnvlem  43986  nzss  44290  supminfxr  45444  dvnprodlem1  45928  dvnprodlem2  45929  dvnprodlem3  45930  dvnprod  45931  stoweidlem26  46008  stoweidlem27  46009  stoweidlem31  46013  stoweidlem34  46016  stoweidlem46  46028  fourierdlem79  46167  fourierdlem96  46184  fourierdlem97  46185  fourierdlem98  46186  fourierdlem99  46187  fourierdlem105  46193  fourierdlem107  46195  fourierdlem108  46196  fourierdlem110  46198  etransclem11  46227  salgenval  46303  subsaliuncl  46340  ovnval  46523  ovnval2  46527  ovnval2b  46534  ovncvrrp  46546  ovnsubaddlem1  46552  ovnsubadd  46554  ovncvr2  46593  hspmbl  46611  ovolval2  46626  ovnovollem3  46640  salpreimagelt  46689  salpreimalegt  46691  salpreimagtge  46707  salpreimaltle  46708  issmflem  46709  issmf  46710  salpreimagtlt  46712  smfpreimalt  46713  smfpreimaltf  46718  issmfle  46727  smfpimltxr  46729  smfpreimale  46736  issmfgt  46738  smfpreimagt  46744  issmfge  46752  smflimlem3  46755  smflimlem4  46756  smflim  46759  smfpimgtxr  46762  smfpreimage  46764  fvmptrabdm  47278  elsetpreimafveq  47382  prmdvdsfmtnof1  47572  fppr  47711  dfclnbgr2  47808  dfclnbgr3  47811  dfsclnbgr6  47843  grlimedgclnbgr  47980  grlimgrtri  47988  grilcbri2  47996  bigoval  48535  line  48718  rrxline  48720  sphere  48733  line2y  48741  inpw  48810