Theorem rabbidva 3415

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3408

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-rab 3409

This theorem is referenced by:  rabbidv  3416  rabeqbidva  3425  rabeqbidvaOLD  3426  rabbi2dva  4192  rabxfrd  5375  seinxp  5725  ordintdif  6386  f1oresrab  7102  onsucmin  7799  suppval1  8148  mptsuppd  8169  naddasslem1  8661  naddasslem2  8662  naddsuc2  8668  cantnflem1  9649  harsucnn  9958  dfinfre  12171  ixxin  13330  mptnn0fsuppr  13971  scshwfzeqfzo  14799  incexc2  15811  smueqlem  16467  gcdass  16524  lcmass  16591  pcneg  16852  ramval  16986  acsfn  17627  monpropd  17706  f1omvdcnv  19381  pmtrmvd  19393  submod  19506  odngen  19514  sylow3lem6  19569  efgsfo  19676  rrgsupp  20617  acsfn1p  20715  rngqiprngimf1  21217  dsmmbas2  21653  dsmmacl  21657  frlmbas  21671  frlmsslss2  21691  mplsubglem2  21917  ltbwe  21958  coe1mul2lem2  22161  scmatmats  22405  mretopd  22986  ordtbaslem  23082  ordtrest  23096  ordtrest2lem  23097  leordtval  23107  xkopt  23549  xkoco1cn  23551  xkoco2cn  23552  xkoinjcn  23581  r0cld  23632  utopsnneiplem  24142  stdbdbl  24412  minveclem3b  25335  minveclem4  25339  lhop1lem  25925  idomrootle  26085  mumul  27098  sqff1o  27099  lgsquadlem1  27298  lgsquadlem2  27299  2lgslem1a  27309  lrrecse  27856  lrrecpred  27858  elntg2  28919  edglnl  29077  nbupgr  29278  vtxdun  29416  wwlksnextprop  29849  wpthswwlks2on  29898  rusgrnumwwlkslem  29906  rusgrnumwwlks  29911  clwlknf1oclwwlkn  30020  frcond3  30205  extwwlkfab  30288  grpoidinv2  30451  grpoinv  30461  xppreima  32576  qusker  33327  nsgqusf1olem3  33393  fedgmullem2  33633  ply1annidllem  33698  zarclsun  33867  cnvordtrestixx  33910  ordtrestNEW  33918  ordtrest2NEWlem  33919  fnrelpredd  35086  satfv1lem  35356  satefvfmla0  35412  satefvfmla1  35419  lineunray  36142  lineelsb2  36143  linecom  36145  ee7.2aOLD  36456  poimirlem26  37647  poimirlem27  37648  mbfposadd  37668  cnambfre  37669  itg2addnclem2  37673  iblabsnclem  37684  ftc1anclem1  37694  lfl1dim2N  39122  pmapat  39764  pmapglbx  39770  dvhb1dimN  40987  dia0  41053  mapdval2N  41631  mapdsn  41642  hlhilocv  41958  isprimroot  42088  aks6d1c6isolem3  42171  unitscyglem5  42194  istopclsd  42695  diophren  42808  rabrenfdioph  42809  pwfi2f1o  43092  idomodle  43187  hausgraph  43201  nadd1rabtr  43384  nadd1rabex  43386  nadd1suc  43388  minregex2  43531  fsovcnvlem  44009  ntrneifv3  44078  ntrneifv4  44081  clsneifv3  44106  clsneifv4  44107  neicvgfv  44117  nzss  44313  preimaiocmnf  45565  preimaicomnf  46716  smfsupxr  46821  smfliminflem  46835  sprvalpwle2  47494  fpprmod  47732  dfsclnbgr2  47850  dfvopnbgr2  47857  uspgrlimlem2  47992  rmsupp0  48360  lco0  48420  rrxlinesc  48728  rrxlinec  48729  rrx2line  48733  rrx2vlinest  48734  rrx2linest  48735  rrx2linesl  48736  rrx2linest2  48737  2sphere  48742  2sphere0  48743  line2  48745  itsclinecirc0b  48767