Theorem rabbii 3442

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3444. (Contributed by Peter Mazsa, 1-Nov-2019.)

Hypothesis

Ref	Expression
rabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rabbii	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem rabbii

Step	Hyp	Ref	Expression
1		rabbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rabbiia 3440	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  {crab 3436

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-rab 3437

This theorem is referenced by:  rabbieq  3445  dfdif3OLD  4118  elneldisj  4392  elnelun  4393  dfepfr  5669  epfrc  5670  fndmdifcom  7063  fniniseg2  7082  uniordint  7821  naddov3  8718  dfoi  9551  kmlem3  10193  alephsuc3  10620  hashbclem  14491  gcdcom  16550  gcdass  16584  lcmcom  16630  lcmass  16651  acsfn0  17703  dfinito2  18048  dftermo2  18049  dfrhm2  20474  lbsextg  21164  dmtopon  22929  fctop2  23012  ordtrest2  23212  qtopres  23706  tsmsfbas  24136  shftmbl  25573  ppiub  27248  rpvmasum  27570  noextendlt  27714  nosepne  27725  nosepdm  27729  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  umgrislfupgrlem  29139  finsumvtxdg2ssteplem1  29563  clwwlknclwwlkdifnum  29999  clwwlknon2num  30124  dlwwlknondlwlknonf1o  30384  numclwlk1lem1  30388  3unrab  32522  aciunf1  32673  fpwrelmapffslem  32743  ordtrest2NEW  33922  unelldsys  34159  rossros  34181  aean  34245  orvcval2  34461  subfacp1lem6  35190  satfv1  35368  itg2addnclem2  37679  scottexf  38175  scott0f  38176  refsymrels2  38566  dfeqvrels2  38589  refrelsredund3  38635  dffunsALTV5  38688  glbconxN  39380  primrootsunit1  42098  primrootsunit  42099  3anrabdioph  42793  3orrabdioph  42794  rexrabdioph  42805  2rexfrabdioph  42807  3rexfrabdioph  42808  4rexfrabdioph  42809  6rexfrabdioph  42810  7rexfrabdioph  42811  elnn0rabdioph  42814  elnnrabdioph  42818  rabren3dioph  42826  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  onuniintrab  43238  relintab  43596  sqrtcvallem1  43644  uzmptshftfval  44365  binomcxplemdvsum  44374  binomcxp  44376  dvnprod  45964  ovnsubadd  46587  hoidmv1lelem3  46608  hoidmvlelem3  46612  ovolval3  46662  ovolval4lem2  46665  ovolval5lem3  46669  smflimlem4  46789