Theorem rabbidva 3418

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-rab 3413

This theorem is used by:  rabbidv  3419  rabeqbidva  3428  rabbi2dva  4121  rabxfrd  5379  seinxp  5736  ordintdif  6417  f1oresrab  7133  onsucmin  7836  suppval1  8190  mptsuppd  8211  naddasslem1  8711  naddasslem2  8712  naddsuc2  8718  cantnflem1  9697  harsucnn  10086  dfinfre  12305  ixxin  13500  mptnn0fsuppr  14149  scshwfzeqfzo  14985  incexc2  16016  smueqlem  16669  gcdass  16729  lcmass  16798  pcneg  17061  ramval  17195  acsfn  17842  monpropd  17921  f1omvdcnv  19667  pmtrmvd  19679  submod  19792  odngen  19800  sylow3lem6  19855  efgsfo  19962  rrgsupp  20962  acsfn1p  21065  rngqiprngimf1  21605  dsmmbas2  22052  dsmmacl  22056  frlmbas  22070  frlmsslss2  22090  mplsubglem2  22317  ltbwe  22362  coe1mul2lem2  22596  scmatmats  22835  mretopd  23419  ordtbaslem  23515  ordtrest  23529  ordtrest2lem  23530  leordtval  23540  xkopt  23983  xkoco1cn  23985  xkoco2cn  23986  xkoinjcn  24015  r0cld  24066  utopsnneiplem  24575  stdbdbl  24845  minveclem3b  25758  minveclem4  25762  lhop1lem  26342  idomrootle  26500  mumul  27517  sqff1o  27518  lgsquadlem1  27716  lgsquadlem2  27717  2lgslem1a  27727  lrrecse  28337  lrrecpred  28339  plngcplem  29272  elntg2  29572  edglnl  29730  nbupgr  29934  vtxdun  30071  wwlksnextprop  30510  wpthswwlks2on  30562  rusgrnumwwlkslem  30570  rusgrnumwwlks  30575  clwlknf1oclwwlkn  30684  frcond3  30879  extwwlkfab  30962  grpoidinv2  31126  grpoinv  31136  xppreima  33290  qusker  33960  nsgqusf1olem3  34016  fedgmullem2  34312  ply1annidllem  34383  zarclsun  34552  cnvordtrestixx  34595  ordtrestNEW  34603  ordtrest2NEWlem  34604  fnrelpredd  35776  fineqvnttrclse  35852  satfv1lem  36217  satefvfmla0  36273  satefvfmla1  36280  lineunray  37008  lineelsb2  37009  linecom  37011  nmulrid  37042  ee7.2aOLD  37345  poimirlem26  38673  poimirlem27  38674  mbfposadd  38694  cnambfre  38695  itg2addnclem2  38699  iblabsnclem  38710  ftc1anclem1  38720  lfl1dim2N  40288  pmapat  40929  pmapglbx  40935  dvhb1dimN  42152  dia0  42218  mapdval2N  42796  mapdsn  42807  hlhilocv  43123  isprimroot  43252  aks6d1c6isolem3  43335  unitscyglem5  43358  frlmnzcoordsca  43767  istopclsd  43820  diophren  43929  rabrenfdioph  43930  pwfi2f1o  44207  idomodle  44302  hausgraph  44316  nadd1rabtr  44499  nadd1rabex  44501  nadd1suc  44503  minregex2  44645  fsovcnvlem  45122  ntrneifv3  45191  ntrneifv4  45194  clsneifv3  45219  clsneifv4  45220  neicvgfv  45230  nzss  45410  preimaiocmnf  46680  preimaicomnf  47829  smfsupxr  47934  smfliminflem  47948  sprvalpwle2  48679  fpprmod  48933  dfsclnbgr2  49052  dfvopnbgr2  49059  uspgrlimlem2  49195  rmsupp0  49588  lco0  49647  rrxlinesc  49956  rrxlinec  49957  rrx2line  49960  rrx2vlinest  49961  rrx2linest  49962  rrx2linesl  49963  rrx2linest2  49964  2sphere  49969  2sphere0  49970  line2  49972  itsclinecirc0b  49994