Theorem ralbii 2476

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 2470	. 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1357	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 104  ⊤wtru 1349  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-ral 2453

This theorem is referenced by:  2ralbii  2478  ralinexa  2497  r3al  2514  r19.26-2  2599  r19.26-3  2600  ralbiim  2604  r19.28av  2606  ralnex2  2609  cbvral2vw  2707  cbvral2v  2709  cbvral3v  2711  sbralie  2714  ralcom4  2752  reu8  2926  2reuswapdc  2934  r19.12sn  3649  eqsnm  3742  uni0b  3821  uni0c  3822  ssint  3847  iuniin  3883  iuneq2  3889  iunss  3914  ssiinf  3922  iinab  3934  iindif2m  3940  iinin2m  3941  iinuniss  3955  sspwuni  3957  iinpw  3963  dftr3  4091  trint  4102  bnd2  4159  reusv3  4445  reg2exmidlema  4518  setindel  4522  ordsoexmid  4546  zfregfr  4558  tfi  4566  tfis2f  4568  ssrel2  4701  reliun  4732  xpiindim  4748  ralxpf  4757  dfse2  4984  rninxp  5054  dminxp  5055  cnviinm  5152  cnvpom  5153  cnvsom  5154  dffun9  5227  funco  5238  funcnv3  5260  fncnv  5264  funimaexglem  5281  fnres  5314  fnopabg  5321  mptfng  5323  fintm  5383  f1ompt  5647  idref  5736  dff13f  5749  foov  5999  tfr1onlemaccex  6327  tfrcllembxssdm  6335  tfrcllemaccex  6340  oacl  6439  ixpeq2  6690  ixpin  6701  ixpiinm  6702  infmoti  7005  acfun  7184  exmidontriimlem1  7198  exmidontriimlem3  7200  ccfunen  7226  cc2  7229  cc4f  7231  cc4n  7233  cauappcvgprlemladdrl  7619  axcaucvglemres  7861  axpre-suploc  7864  dfinfre  8872  suprzclex  9310  supinfneg  9554  infsupneg  9555  cvg1nlemcau  10948  cvg1nlemres  10949  rexfiuz  10953  recvguniq  10959  resqrexlemglsq  10986  resqrexlemsqa  10988  resqrexlemex  10989  clim0  11248  mertenslem2  11499  infssuzex  11904  bezoutlemmain  11953  ennnfoneleminc  12366  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemr  12378  ctinfom  12383  isbasis2g  12837  tgval2  12845  ntreq0  12926  lmres  13042  eltx  13053  suplociccreex  13396  decidi  13830  nninfsellemqall  14048  nninfomni  14052  trirec0xor  14077