Theorem rabbii 3449

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3451. (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 3447	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = 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-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-rab 3444

This theorem is referenced by:  rabbieq  3452  dfdif3OLD  4141  elneldisj  4415  elnelun  4416  dfepfr  5684  epfrc  5685  fndmdifcom  7076  fniniseg2  7095  uniordint  7837  naddov3  8736  dfoi  9580  kmlem3  10222  alephsuc3  10649  hashbclem  14501  gcdcom  16559  gcdass  16594  lcmcom  16640  lcmass  16661  acsfn0  17718  dfinito2  18070  dftermo2  18071  dfrhm2  20500  lbsextg  21187  dmtopon  22950  fctop2  23033  ordtrest2  23233  qtopres  23727  tsmsfbas  24157  shftmbl  25592  ppiub  27266  rpvmasum  27588  noextendlt  27732  nosepne  27743  nosepdm  27747  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem4  27799  umgrislfupgrlem  29157  finsumvtxdg2ssteplem1  29581  clwwlknclwwlkdifnum  30012  clwwlknon2num  30137  dlwwlknondlwlknonf1o  30397  numclwlk1lem1  30401  3unrab  32531  aciunf1  32681  fpwrelmapffslem  32746  ordtrest2NEW  33869  unelldsys  34122  rossros  34144  aean  34208  orvcval2  34423  subfacp1lem6  35153  satfv1  35331  itg2addnclem2  37632  scottexf  38128  scott0f  38129  refsymrels2  38521  dfeqvrels2  38544  refrelsredund3  38590  dffunsALTV5  38643  glbconxN  39335  primrootsunit1  42054  primrootsunit  42055  3anrabdioph  42738  3orrabdioph  42739  rexrabdioph  42750  2rexfrabdioph  42752  3rexfrabdioph  42753  4rexfrabdioph  42754  6rexfrabdioph  42755  7rexfrabdioph  42756  elnn0rabdioph  42759  elnnrabdioph  42763  rabren3dioph  42771  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  onuniintrab  43187  relintab  43545  sqrtcvallem1  43593  uzmptshftfval  44315  binomcxplemdvsum  44324  binomcxp  44326  dvnprod  45870  ovnsubadd  46493  hoidmv1lelem3  46514  hoidmvlelem3  46518  ovolval3  46568  ovolval4lem2  46571  ovolval5lem3  46575  smflimlem4  46695