Theorem rabbii 3406

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2110  {crab 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-rab 3075

This theorem is referenced by:  dfdif3  4054  elneldisj  4328  elnelun  4329  dfepfr  5575  epfrc  5576  fndmdifcom  6917  fniniseg2  6936  uniordint  7645  dfoi  9248  kmlem3  9909  alephsuc3  10337  hashbclem  14162  gcdcom  16218  gcdass  16253  lcmcom  16296  lcmass  16317  acsfn0  17367  dfinito2  17716  dftermo2  17717  dfrhm2  19959  lbsextg  20422  dmtopon  22070  fctop2  22153  ordtrest2  22353  qtopres  22847  tsmsfbas  23277  shftmbl  24700  ppiub  26350  rpvmasum  26672  umgrislfupgrlem  27490  finsumvtxdg2ssteplem1  27910  clwwlknclwwlkdifnum  28340  clwwlknon2num  28465  dlwwlknondlwlknonf1o  28725  numclwlk1lem1  28729  aciunf1  30996  fpwrelmapffslem  31063  ordtrest2NEW  31869  unelldsys  32122  rossros  32144  aean  32208  orvcval2  32421  subfacp1lem6  33143  satfv1  33321  noextendlt  33868  nosepne  33879  nosepdm  33883  nosupbnd2lem1  33914  noinfbnd2lem1  33929  noetasuplem4  33935  itg2addnclem2  35825  scottexf  36322  scott0f  36323  rabbieq  36386  refsymrels2  36675  dfeqvrels2  36697  refrelsredund3  36743  dffunsALTV5  36794  glbconxN  37388  3anrabdioph  40601  3orrabdioph  40602  rexrabdioph  40613  2rexfrabdioph  40615  3rexfrabdioph  40616  4rexfrabdioph  40617  6rexfrabdioph  40618  7rexfrabdioph  40619  elnn0rabdioph  40622  elnnrabdioph  40626  rabren3dioph  40634  rmydioph  40833  rmxdioph  40835  expdiophlem2  40841  relintab  41161  sqrtcvallem1  41209  uzmptshftfval  41934  binomcxplemdvsum  41943  binomcxp  41945  dvnprod  43461  ovnsubadd  44081  hoidmv1lelem3  44102  hoidmvlelem3  44106  ovolval3  44156  ovolval4lem2  44159  ovolval5lem3  44163  smflimlem4  44277