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  3647  eqsnm  3740  uni0b  3819  uni0c  3820  ssint  3845  iuniin  3881  iuneq2  3887  iunss  3912  ssiinf  3920  iinab  3932  iindif2m  3938  iinin2m  3939  iinuniss  3953  sspwuni  3955  iinpw  3961  dftr3  4089  trint  4100  bnd2  4157  reusv3  4443  reg2exmidlema  4516  setindel  4520  ordsoexmid  4544  zfregfr  4556  tfi  4564  tfis2f  4566  ssrel2  4699  reliun  4730  xpiindim  4746  ralxpf  4755  dfse2  4982  rninxp  5052  dminxp  5053  cnviinm  5150  cnvpom  5151  cnvsom  5152  dffun9  5225  funco  5236  funcnv3  5258  fncnv  5262  funimaexglem  5279  fnres  5312  fnopabg  5319  mptfng  5321  fintm  5381  f1ompt  5644  idref  5733  dff13f  5746  foov  5996  tfr1onlemaccex  6324  tfrcllembxssdm  6332  tfrcllemaccex  6337  oacl  6436  ixpeq2  6686  ixpin  6697  ixpiinm  6698  infmoti  7001  acfun  7171  exmidontriimlem1  7185  exmidontriimlem3  7187  ccfunen  7213  cc2  7216  cc4f  7218  cc4n  7220  cauappcvgprlemladdrl  7606  axcaucvglemres  7848  axpre-suploc  7851  dfinfre  8859  suprzclex  9297  supinfneg  9541  infsupneg  9542  cvg1nlemcau  10935  cvg1nlemres  10936  rexfiuz  10940  recvguniq  10946  resqrexlemglsq  10973  resqrexlemsqa  10975  resqrexlemex  10976  clim0  11235  mertenslem2  11486  infssuzex  11891  bezoutlemmain  11940  ennnfoneleminc  12353  ennnfonelemex  12356  ennnfonelemhom  12357  ennnfonelemr  12365  ctinfom  12370  isbasis2g  12758  tgval2  12766  ntreq0  12847  lmres  12963  eltx  12974  suplociccreex  13317  decidi  13751  nninfsellemqall  13970  nninfomni  13974  trirec0xor  13999