Theorem rabbidva 3450

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rab 3444

This theorem is referenced by:  rabbidv  3451  rabeqbidva  3460  rabeqbidvaOLD  3461  rabbi2dva  4247  rabxfrd  5435  seinxp  5783  ordintdif  6445  f1oresrab  7161  onsucmin  7857  suppval1  8207  mptsuppd  8228  naddasslem1  8750  naddasslem2  8751  naddsuc2  8757  cantnflem1  9758  harsucnn  10067  dfinfre  12276  ixxin  13424  mptnn0fsuppr  14050  scshwfzeqfzo  14875  incexc2  15886  smueqlem  16536  gcdass  16594  lcmass  16661  pcneg  16921  ramval  17055  acsfn  17717  monpropd  17798  f1omvdcnv  19486  pmtrmvd  19498  submod  19611  odngen  19619  sylow3lem6  19674  efgsfo  19781  rrgsupp  20723  acsfn1p  20822  rngqiprngimf1  21333  dsmmbas2  21780  dsmmacl  21784  frlmbas  21798  frlmsslss2  21818  mplsubglem2  22044  ltbwe  22085  coe1mul2lem2  22292  scmatmats  22538  mretopd  23121  ordtbaslem  23217  ordtrest  23231  ordtrest2lem  23232  leordtval  23242  xkopt  23684  xkoco1cn  23686  xkoco2cn  23687  xkoinjcn  23716  r0cld  23767  utopsnneiplem  24277  stdbdbl  24551  minveclem3b  25481  minveclem4  25485  lhop1lem  26072  idomrootle  26232  mumul  27242  sqff1o  27243  lgsquadlem1  27442  lgsquadlem2  27443  2lgslem1a  27453  lrrecse  27993  lrrecpred  27995  elntg2  29018  edglnl  29178  nbupgr  29379  vtxdun  29517  wwlksnextprop  29945  wpthswwlks2on  29994  rusgrnumwwlkslem  30002  rusgrnumwwlks  30007  clwlknf1oclwwlkn  30116  frcond3  30301  extwwlkfab  30384  grpoidinv2  30547  grpoinv  30557  xppreima  32664  qusker  33342  nsgqusf1olem3  33408  fedgmullem2  33643  ply1annidllem  33694  zarclsun  33816  cnvordtrestixx  33859  ordtrestNEW  33867  ordtrest2NEWlem  33868  fnrelpredd  35065  satfv1lem  35330  satefvfmla0  35386  satefvfmla1  35393  lineunray  36111  lineelsb2  36112  linecom  36114  ee7.2aOLD  36427  poimirlem26  37606  poimirlem27  37607  mbfposadd  37627  cnambfre  37628  itg2addnclem2  37632  iblabsnclem  37643  ftc1anclem1  37653  lfl1dim2N  39078  pmapat  39720  pmapglbx  39726  dvhb1dimN  40943  dia0  41009  mapdval2N  41587  mapdsn  41598  hlhilocv  41918  isprimroot  42050  aks6d1c6isolem3  42133  unitscyglem5  42156  istopclsd  42656  diophren  42769  rabrenfdioph  42770  pwfi2f1o  43053  idomodle  43152  hausgraph  43166  nadd1rabtr  43350  nadd1rabex  43352  nadd1suc  43354  minregex2  43497  fsovcnvlem  43975  ntrneifv3  44044  ntrneifv4  44047  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  nzss  44286  preimaiocmnf  45479  preimaicomnf  46632  smfsupxr  46737  smfliminflem  46751  sprvalpwle2  47363  fpprmod  47601  dfsclnbgr2  47718  dfvopnbgr2  47725  uspgrlimlem2  47813  rmsupp0  48093  lco0  48156  rrxlinesc  48469  rrxlinec  48470  rrx2line  48474  rrx2vlinest  48475  rrx2linest  48476  rrx2linesl  48477  rrx2linest2  48478  2sphere  48483  2sphere0  48484  line2  48486  itsclinecirc0b  48508