Theorem rabbidva 3478

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-rab 3147

This theorem is referenced by:  rabbidv  3480  rabeqbidva  3486  rabbi2dva  4193  rabxfrd  5309  seinxp  5629  ordintdif  6234  f1oresrab  6883  onsucmin  7530  suppval1  7830  mptsuppd  7847  cantnflem1  9146  dfinfre  11616  ixxin  12749  mptnn0fsuppr  13361  scshwfzeqfzo  14182  incexc2  15187  smueqlem  15833  gcdass  15889  lcmass  15952  pcneg  16204  ramval  16338  acsfn  16924  monpropd  17001  f1omvdcnv  18566  pmtrmvd  18578  submod  18688  odngen  18696  sylow3lem6  18751  efgsfo  18859  acsfn1p  19572  rrgsupp  20058  mplsubglem2  20210  ltbwe  20247  mhpinvcl  20333  coe1mul2lem2  20430  dsmmbas2  20875  dsmmacl  20879  frlmbas  20893  frlmsslss2  20913  scmatmats  21114  mretopd  21694  ordtbaslem  21790  ordtrest  21804  ordtrest2lem  21805  leordtval  21815  xkopt  22257  xkoco1cn  22259  xkoco2cn  22260  xkoinjcn  22289  r0cld  22340  utopsnneiplem  22850  stdbdbl  23121  minveclem3b  24025  minveclem4  24029  lhop1lem  24604  mumul  25752  sqff1o  25753  lgsquadlem1  25950  lgsquadlem2  25951  2lgslem1a  25961  elntg2  26765  edglnl  26922  nbupgr  27120  vtxdun  27257  wwlksnextprop  27685  wpthswwlks2on  27734  rusgrnumwwlkslem  27742  rusgrnumwwlks  27747  clwlknf1oclwwlkn  27857  frcond3  28042  extwwlkfab  28125  grpoidinv2  28286  grpoinv  28296  xppreima  30388  qusker  30913  fedgmullem2  31021  cnvordtrestixx  31151  ordtrestNEW  31159  ordtrest2NEWlem  31160  satfv1lem  32604  satefvfmla0  32660  satefvfmla1  32667  lineunray  33603  lineelsb2  33604  linecom  33606  ee7.2aOLD  33804  poimirlem26  34912  poimirlem27  34913  mbfposadd  34933  cnambfre  34934  itg2addnclem2  34938  iblabsnclem  34949  ftc1anclem1  34961  lfl1dim2N  36252  pmapat  36893  pmapglbx  36899  dvhb1dimN  38116  dia0  38182  mapdval2N  38760  mapdsn  38771  hlhilocv  39087  istopclsd  39290  diophren  39403  rabrenfdioph  39404  pwfi2f1o  39689  idomrootle  39788  idomodle  39789  hausgraph  39805  harsucnn  39896  fsovcnvlem  40352  ntrneifv3  40425  ntrneifv4  40428  clsneifv3  40453  clsneifv4  40454  neicvgfv  40464  nzss  40642  preimaiocmnf  41830  preimaicomnf  42984  smfsupxr  43084  smfliminflem  43098  sprvalpwle2  43645  fpprmod  43886  rmsupp0  44410  lco0  44476  rrxlinesc  44716  rrxlinec  44717  rrx2line  44721  rrx2vlinest  44722  rrx2linest  44723  rrx2linesl  44724  rrx2linest2  44725  2sphere  44730  2sphere0  44731  line2  44733  itsclinecirc0b  44755