Theorem rabbidva 3439

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.)

Hypothesis

Ref	Expression
rabbidva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabbidva	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidva

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 579	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3434	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-rab 3433

This theorem is referenced by:  rabbidv  3440  rabeqbidva  3448  rabbi2dva  4217  rabxfrd  5415  seinxp  5759  ordintdif  6414  f1oresrab  7127  onsucmin  7811  suppval1  8154  mptsuppd  8174  naddasslem1  8695  naddasslem2  8696  cantnflem1  9686  harsucnn  9995  dfinfre  12197  ixxin  13343  mptnn0fsuppr  13966  scshwfzeqfzo  14779  incexc2  15786  smueqlem  16433  gcdass  16491  lcmass  16553  pcneg  16809  ramval  16943  acsfn  17605  monpropd  17686  f1omvdcnv  19314  pmtrmvd  19326  submod  19439  odngen  19447  sylow3lem6  19502  efgsfo  19609  acsfn1p  20419  rrgsupp  20913  dsmmbas2  21298  dsmmacl  21302  frlmbas  21316  frlmsslss2  21336  mplsubglem2  21566  ltbwe  21605  coe1mul2lem2  21797  scmatmats  22020  mretopd  22603  ordtbaslem  22699  ordtrest  22713  ordtrest2lem  22714  leordtval  22724  xkopt  23166  xkoco1cn  23168  xkoco2cn  23169  xkoinjcn  23198  r0cld  23249  utopsnneiplem  23759  stdbdbl  24033  minveclem3b  24952  minveclem4  24956  lhop1lem  25537  mumul  26692  sqff1o  26693  lgsquadlem1  26890  lgsquadlem2  26891  2lgslem1a  26901  lrrecse  27435  lrrecpred  27437  elntg2  28281  edglnl  28441  nbupgr  28639  vtxdun  28776  wwlksnextprop  29204  wpthswwlks2on  29253  rusgrnumwwlkslem  29261  rusgrnumwwlks  29266  clwlknf1oclwwlkn  29375  frcond3  29560  extwwlkfab  29643  grpoidinv2  29806  grpoinv  29816  xppreima  31909  qusker  32505  nsgqusf1olem3  32571  fedgmullem2  32774  ply1annidllem  32822  zarclsun  32919  cnvordtrestixx  32962  ordtrestNEW  32970  ordtrest2NEWlem  32971  fnrelpredd  34161  satfv1lem  34422  satefvfmla0  34478  satefvfmla1  34485  lineunray  35188  lineelsb2  35189  linecom  35191  ee7.2aOLD  35432  poimirlem26  36600  poimirlem27  36601  mbfposadd  36621  cnambfre  36622  itg2addnclem2  36626  iblabsnclem  36637  ftc1anclem1  36647  lfl1dim2N  38078  pmapat  38720  pmapglbx  38726  dvhb1dimN  39943  dia0  40009  mapdval2N  40587  mapdsn  40598  hlhilocv  40918  istopclsd  41520  diophren  41633  rabrenfdioph  41634  pwfi2f1o  41920  idomrootle  42019  idomodle  42020  hausgraph  42036  nadd1rabtr  42220  nadd1rabex  42222  nadd1suc  42224  naddsuc2  42225  minregex2  42368  fsovcnvlem  42846  ntrneifv3  42915  ntrneifv4  42918  clsneifv3  42943  clsneifv4  42944  neicvgfv  42954  nzss  43158  preimaiocmnf  44353  preimaicomnf  45506  smfsupxr  45611  smfliminflem  45625  sprvalpwle2  46236  fpprmod  46474  rngqiprngimf1  46864  rmsupp0  47123  lco0  47186  rrxlinesc  47499  rrxlinec  47500  rrx2line  47504  rrx2vlinest  47505  rrx2linest  47506  rrx2linesl  47507  rrx2linest2  47508  2sphere  47513  2sphere0  47514  line2  47516  itsclinecirc0b  47538