Theorem rabbii 3411

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 3409	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3405

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3406

This theorem is referenced by:  rabbieq  3414  dfdif3OLD  4081  elneldisj  4355  elnelun  4356  dfepfr  5622  epfrc  5623  fndmdifcom  7015  fniniseg2  7034  uniordint  7777  naddov3  8644  dfoi  9464  kmlem3  10106  alephsuc3  10533  hashbclem  14417  gcdcom  16483  gcdass  16517  lcmcom  16563  lcmass  16584  acsfn0  17621  dfinito2  17965  dftermo2  17966  dfrhm2  20383  lbsextg  21072  dmtopon  22810  fctop2  22892  ordtrest2  23091  qtopres  23585  tsmsfbas  24015  shftmbl  25439  ppiub  27115  rpvmasum  27437  noextendlt  27581  nosepne  27592  nosepdm  27596  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem4  27648  umgrislfupgrlem  29049  finsumvtxdg2ssteplem1  29473  clwwlknclwwlkdifnum  29909  clwwlknon2num  30034  dlwwlknondlwlknonf1o  30294  numclwlk1lem1  30298  3unrab  32432  aciunf1  32587  fpwrelmapffslem  32655  constrcbvlem  33745  ordtrest2NEW  33913  unelldsys  34148  rossros  34170  aean  34234  orvcval2  34450  subfacp1lem6  35172  satfv1  35350  itg2addnclem2  37666  scottexf  38162  scott0f  38163  refsymrels2  38556  dfeqvrels2  38579  refrelsredund3  38625  dffunsALTV5  38679  glbconxN  39372  primrootsunit1  42085  primrootsunit  42086  3anrabdioph  42770  3orrabdioph  42771  rexrabdioph  42782  2rexfrabdioph  42784  3rexfrabdioph  42785  4rexfrabdioph  42786  6rexfrabdioph  42787  7rexfrabdioph  42788  elnn0rabdioph  42791  elnnrabdioph  42795  rabren3dioph  42803  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  onuniintrab  43215  relintab  43572  sqrtcvallem1  43620  uzmptshftfval  44335  binomcxplemdvsum  44344  binomcxp  44346  dvnprod  45947  ovnsubadd  46570  hoidmv1lelem3  46591  hoidmvlelem3  46595  ovolval3  46645  ovolval4lem2  46648  ovolval5lem3  46652  smflimlem4  46772