Theorem rabbidv 3438

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 479	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
3	2	rabbidva 3437	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  {crab 3430

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-rab 3431

This theorem is referenced by:  difeq2  4115  seex  5637  mptiniseg  6237  dfpred3g  6311  elovmporab  7654  elovmpt3rab1  7668  naddcllem  8677  naddov2  8680  naddcom  8683  naddrid  8684  naddass  8697  fineqvlem  9264  mapfien2  9406  supeq1  9442  supeq2  9445  supeq3  9446  oieq1  9509  oieq2  9510  ordtypecbv  9514  ordtypelem3  9517  harval  9557  inf3lema  9621  wemapwe  9694  oef1o  9695  tz9.12lem3  9786  rankvalb  9794  rankvalg  9814  ranksnb  9824  rankonidlem  9825  cardval3  9949  cardidm  9956  alephsuc2  10077  coftr  10270  fin1a2lem11  10407  fin1a2lem12  10408  hsmex  10429  axdc3lem2  10448  zorn2lem1  10493  zorn2lem6  10498  zorn2lem7  10499  zorn2g  10500  wuncval  10739  tskmval  10836  peano5uzti  12656  uzval  12828  rpnnen1  12971  ixxval  13336  fzval  13490  hashbclem  14415  hashbc  14416  shftfn  15024  bitsfval  16368  sadfval  16397  sadcom  16408  smufval  16422  smupp1  16425  smupval  16433  smumullem  16437  gcdval  16441  bezoutlem2  16486  bezoutlem4  16488  lcmval  16533  lcmfval  16562  lcmf0val  16563  lcmfpr  16568  isprm  16614  odzval  16728  pcval  16781  pceulem  16782  pceu  16783  pczpre  16784  pcdiv  16789  prmreclem1  16853  prmreclem4  16856  prmreclem5  16857  ramval  16945  cshws0  17039  imasdsval  17465  mrcval  17558  eldmcoa  18019  cycsubg2  19125  cntzval  19226  cntzsnval  19229  odfval  19441  odfvalALT  19442  odval  19443  gexval  19487  efgsfo  19648  dprdval  19914  ablfac1a  19980  ablfac1b  19981  ablfac1eu  19984  ablfaclem1  19996  ablfaclem3  19998  rnghmval  20331  lspval  20730  ocvval  21439  dsmmelbas  21513  frlmsslss  21548  aspval  21646  psrass1lemOLD  21712  psrass1lem  21715  psrmulval  21724  mplmonmul  21810  mhpval  21902  mhpmulcl  21911  coe1mul2  22011  pmatcoe1fsupp  22423  istopon  22634  toponsspwpw  22644  clsval  22761  neival  22826  ordtbaslem  22912  ordtbas2  22915  ordtopn1  22918  ordtopn2  22919  cnpval  22960  llyeq  23194  nllyeq  23195  ptfinfin  23243  finlocfin  23244  dissnlocfin  23253  locfindis  23254  xkoopn  23313  kqfval  23447  tsmsfbas  23852  blvalps  24111  blval  24112  nmofval  24451  nmoval  24452  ishtpy  24718  minveclem3b  25176  minveclem3  25177  minveclem4  25180  minveclem5  25181  ovolval  25222  vitalilem2  25358  vitalilem3  25359  vitalilem4  25360  vitali  25362  itg2monolem1  25500  elcpn  25684  mdegmullem  25831  elqaalem1  26068  elqaalem2  26069  elqaalem3  26070  elqaa  26071  aannenlem1  26077  aannenlem2  26078  jensen  26729  vmaval  26853  muval  26872  sgmval  26882  fsumdvdscom  26925  musum  26931  muinv  26933  dchrisum0fval  27244  dchrisum0ff  27246  logsqvma2  27282  pntrlog2bndlem1  27316  scutval  27538  tglngval  28069  ttgval  28393  ttgvalOLD  28394  ttgitvval  28406  ebtwntg  28507  numedglnl  28671  dfnbgr2  28861  dfnbgr3  28862  uvtxusgr  28926  vtxdgval  28992  rusgrnumwrdl2  29110  iswwlksnon  29374  rusgrnumwwlks  29495  hashecclwwlkn1  29597  umgrhashecclwwlk  29598  clwlknf1oclwwlknlem2  29602  clwwlknon  29610  clwwlk0on0  29612  eupth2  29759  fusgreg2wsplem  29853  fusgreghash2wsp  29858  numclwlk1lem1  29889  sspval  30243  ubthlem1  30390  ubthlem2  30391  ubthlem3  30392  ocval  30800  spanval  30853  chsupid  30932  eigvecval  31416  specval  31418  iunpreima  32063  pwrssmgc  32437  nsgqusf1olem3  32800  minplyval  33055  crefeq  33123  zarcls1  33147  zarclsun  33148  zarclsiin  33149  zarclsint  33150  zarclssn  33151  zartop  33154  zartopon  33155  zart0  33157  zarmxt1  33158  zarcmp  33160  rhmpreimacnlem  33162  rhmpreimacn  33163  ordtcnvNEW  33198  ordtrest2NEW  33201  ordtconnlem1  33202  measvuni  33510  brfae  33544  omsfval  33591  orvcelval  33765  ballotlemi  33797  bnj602  34224  subfacp1lem6  34474  kur14  34505  cvmscbv  34547  cvmsi  34554  cvmsval  34555  snmlval  34620  snmlflim  34621  satfv0  34647  satfv1  34652  satfv0fun  34660  satffunlem1lem1  34691  satffunlem2lem1  34693  satfv0fvfmla0  34702  satfv1fvfmla1  34712  prv1n  34720  fvray  35417  fwddifnval  35439  neibastop3  35550  icoreval  36537  fin2so  36778  poimirlem26  36817  poimirlem27  36818  poimirlem28  36819  poimirlem32  36823  ftc1anclem6  36869  islinei  38914  pmapval  38931  paddval  38972  paddcom  38987  pclvalN  39064  ldilset  39283  dilsetN  39327  diafval  40205  diaval  40206  docavalN  40297  dicfval  40349  dochfval  40524  dochval  40525  mapdval  40802  mapdsn2  40816  prjcrvval  41676  2rexfrabdioph  41836  3rexfrabdioph  41837  4rexfrabdioph  41838  6rexfrabdioph  41839  7rexfrabdioph  41840  eldioph4i  41852  diophren  41853  pell1qrval  41886  pell14qrval  41888  pell1234qrval  41890  rpnnen3  42073  fnwe2lem1  42094  pwssplit4  42133  pwslnmlem2  42137  dgraaval  42188  itgoval  42205  rgspnval  42212  proot1hash  42244  rp-intrabeq  42272  rp-unirabeq  42273  rfovfvd  43055  rfovfvfvd  43056  rfovcnvf1od  43057  fsovrfovd  43062  fsovfvd  43063  fsovfvfvd  43064  fsovcnvlem  43066  nzss  43378  supminfxr  44472  dvnprodlem1  44960  dvnprodlem2  44961  dvnprodlem3  44962  dvnprod  44963  stoweidlem26  45040  stoweidlem27  45041  stoweidlem31  45045  stoweidlem34  45048  stoweidlem46  45060  fourierdlem79  45199  fourierdlem96  45216  fourierdlem97  45217  fourierdlem98  45218  fourierdlem99  45219  fourierdlem105  45225  fourierdlem107  45227  fourierdlem108  45228  fourierdlem110  45230  etransclem11  45259  salgenval  45335  subsaliuncl  45372  ovnval  45555  ovnval2  45559  ovnval2b  45566  ovncvrrp  45578  ovnsubaddlem1  45584  ovnsubadd  45586  ovncvr2  45625  hspmbl  45643  ovolval2  45658  ovnovollem3  45672  salpreimagelt  45721  salpreimalegt  45723  salpreimagtge  45739  salpreimaltle  45740  issmflem  45741  issmf  45742  salpreimagtlt  45744  smfpreimalt  45745  smfpreimaltf  45750  issmfle  45759  smfpimltxr  45761  smfpreimale  45768  issmfgt  45770  smfpreimagt  45776  issmfge  45784  smflimlem3  45787  smflimlem4  45788  smflim  45791  smfpimgtxr  45794  smfpreimage  45796  fvmptrabdm  46299  elsetpreimafveq  46363  prmdvdsfmtnof1  46553  fppr  46692  bigoval  47322  line  47505  rrxline  47507  sphere  47520  line2y  47528  inpw  47590