Theorem ralbii 2556

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
ralbii	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	ralbidv 2550	. 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1411	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   ↔ wb 105  ⊤wtru 1403  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-ral 2533

This theorem is used by:  2ralbii  2558  ralinexa  2577  r3al  2594  r19.26-2  2680  r19.26-3  2681  ralbiim  2685  r19.28av  2687  ralnex2  2690  ralrot3  2716  cbvral2vw  2797  cbvral2v  2799  cbvral3v  2801  sbralie  2804  ralcom4  2844  reu8  3022  2reuswapdc  3030  r19.12sn  3775  eqsnm  3880  uni0b  3960  uni0c  3961  ssint  3986  iuniin  4022  iuneq2  4028  iunss  4053  ssiinf  4062  iinab  4074  iindif2m  4080  iinin2m  4081  iinuniss  4095  sspwuni  4097  iinpw  4103  dftr3  4233  trint  4244  bnd2  4310  reusv3  4606  reg2exmidlema  4681  setindel  4685  ordsoexmid  4709  zfregfr  4721  tfi  4729  tfis2f  4731  ssrel2  4865  reliun  4898  xpiindim  4917  ralxpf  4926  dfse2  5160  rninxp  5231  dminxp  5232  cnviinm  5329  cnvpom  5330  cnvsom  5331  dffun9  5406  funco  5417  funcnv3  5443  fncnv  5447  funimaexglem  5464  fnres  5500  fnopabg  5507  mptfng  5509  fintm  5577  f1ompt  5859  idref  5962  dff13f  5976  foov  6236  tfr1onlemaccex  6619  tfrcllembxssdm  6627  tfrcllemaccex  6632  oacl  6733  ixpeq2  6994  ixpin  7005  ixpiinm  7006  infmoti  7369  acfun  7564  exmidontriimlem1  7578  exmidontriimlem3  7580  ccfunen  7631  cc2  7634  cc4f  7636  cc4n  7638  cauappcvgprlemladdrl  8025  axcaucvglemres  8267  axpre-suploc  8270  dfinfre  9289  suprzclex  9749  supinfneg  10005  infsupneg  10006  infssuzex  10677  hashfibc  11299  cvg1nlemcau  11766  cvg1nlemres  11767  rexfiuz  11771  recvguniq  11777  resqrexlemglsq  11804  resqrexlemsqa  11806  resqrexlemex  11807  clim0  12070  mertenslem2  12322  bezoutlemmain  12794  ballotfilem7  13331  ennnfoneleminc  13354  ennnfonelemex  13357  ennnfonelemhom  13358  ennnfonelemr  13366  ctinfom  13371  isnsg2  14059  isbasis2g  15237  tgval2  15243  ntreq0  15324  lmres  15440  eltx  15451  suplociccreex  15816  lgseisenlem2  16356  vtxd0nedgbfi  16706  decidi  16989  nninfsellemqall  17224  nninfomni  17228  trirec0xor  17261  ralsbii  17309  ralseubii  17341