Theorem rabbidva 3419

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-rab 3414

This theorem is used by:  rabbidv  3420  rabeqbidva  3429  rabbi2dva  4171  rabxfrd  5379  seinxp  5735  ordintdif  6413  f1oresrab  7126  onsucmin  7830  suppval1  8176  mptsuppd  8197  naddasslem1  8697  naddasslem2  8698  naddsuc2  8704  cantnflem1  9683  harsucnn  10072  dfinfre  12291  ixxin  13486  mptnn0fsuppr  14135  scshwfzeqfzo  14970  incexc2  16000  smueqlem  16653  gcdass  16713  lcmass  16782  pcneg  17045  ramval  17179  acsfn  17826  monpropd  17905  f1omvdcnv  19651  pmtrmvd  19663  submod  19776  odngen  19784  sylow3lem6  19839  efgsfo  19946  rrgsupp  20946  acsfn1p  21049  rngqiprngimf1  21589  dsmmbas2  22036  dsmmacl  22040  frlmbas  22054  frlmsslss2  22074  mplsubglem2  22301  ltbwe  22346  coe1mul2lem2  22580  scmatmats  22819  mretopd  23403  ordtbaslem  23499  ordtrest  23513  ordtrest2lem  23514  leordtval  23524  xkopt  23967  xkoco1cn  23969  xkoco2cn  23970  xkoinjcn  23999  r0cld  24050  utopsnneiplem  24559  stdbdbl  24829  minveclem3b  25742  minveclem4  25746  lhop1lem  26326  idomrootle  26484  mumul  27501  sqff1o  27502  lgsquadlem1  27700  lgsquadlem2  27701  2lgslem1a  27711  lrrecse  28321  lrrecpred  28323  plngcplem  29256  elntg2  29556  edglnl  29714  nbupgr  29918  vtxdun  30055  wwlksnextprop  30494  wpthswwlks2on  30546  rusgrnumwwlkslem  30554  rusgrnumwwlks  30559  clwlknf1oclwwlkn  30668  frcond3  30863  extwwlkfab  30946  grpoidinv2  31110  grpoinv  31120  xppreima  33232  qusker  33903  nsgqusf1olem3  33959  fedgmullem2  34255  ply1annidllem  34326  zarclsun  34495  cnvordtrestixx  34538  ordtrestNEW  34546  ordtrest2NEWlem  34547  fnrelpredd  35709  fineqvnttrclse  35775  satfv1lem  36106  satefvfmla0  36162  satefvfmla1  36169  lineunray  36892  lineelsb2  36893  linecom  36895  nmulrid  36926  ee7.2aOLD  37229  poimirlem26  38544  poimirlem27  38545  mbfposadd  38565  cnambfre  38566  itg2addnclem2  38570  iblabsnclem  38581  ftc1anclem1  38591  lfl1dim2N  40159  pmapat  40800  pmapglbx  40806  dvhb1dimN  42023  dia0  42089  mapdval2N  42667  mapdsn  42678  hlhilocv  42994  isprimroot  43123  aks6d1c6isolem3  43206  unitscyglem5  43229  frlmnzcoordsca  43638  istopclsd  43690  diophren  43799  rabrenfdioph  43800  pwfi2f1o  44082  idomodle  44177  hausgraph  44191  nadd1rabtr  44374  nadd1rabex  44376  nadd1suc  44378  minregex2  44520  fsovcnvlem  44998  ntrneifv3  45067  ntrneifv4  45070  clsneifv3  45095  clsneifv4  45096  neicvgfv  45106  nzss  45286  preimaiocmnf  46541  preimaicomnf  47690  smfsupxr  47795  smfliminflem  47809  sprvalpwle2  48540  fpprmod  48794  dfsclnbgr2  48913  dfvopnbgr2  48920  uspgrlimlem2  49056  rmsupp0  49449  lco0  49508  rrxlinesc  49816  rrxlinec  49817  rrx2line  49821  rrx2vlinest  49822  rrx2linest  49823  rrx2linesl  49824  rrx2linest2  49825  2sphere  49830  2sphere0  49831  line2  49833  itsclinecirc0b  49855