Theorem ralbii 2550

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

Syntax hints:   ↔ wb 105  ⊤wtru 1399  ∀wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-ral 2527

This theorem is referenced by:  2ralbii  2552  ralinexa  2571  r3al  2588  r19.26-2  2674  r19.26-3  2675  ralbiim  2679  r19.28av  2681  ralnex2  2684  ralrot3  2710  cbvral2vw  2791  cbvral2v  2793  cbvral3v  2795  sbralie  2798  ralcom4  2838  reu8  3016  2reuswapdc  3024  r19.12sn  3760  eqsnm  3864  uni0b  3944  uni0c  3945  ssint  3970  iuniin  4006  iuneq2  4012  iunss  4037  ssiinf  4046  iinab  4058  iindif2m  4064  iinin2m  4065  iinuniss  4079  sspwuni  4081  iinpw  4087  dftr3  4217  trint  4228  bnd2  4291  reusv3  4586  reg2exmidlema  4661  setindel  4665  ordsoexmid  4689  zfregfr  4701  tfi  4709  tfis2f  4711  ssrel2  4845  reliun  4878  xpiindim  4897  ralxpf  4906  dfse2  5140  rninxp  5211  dminxp  5212  cnviinm  5309  cnvpom  5310  cnvsom  5311  dffun9  5386  funco  5397  funcnv3  5423  fncnv  5427  funimaexglem  5444  fnres  5480  fnopabg  5487  mptfng  5489  fintm  5557  f1ompt  5833  idref  5935  dff13f  5949  foov  6209  tfr1onlemaccex  6592  tfrcllembxssdm  6600  tfrcllemaccex  6605  oacl  6706  ixpeq2  6960  ixpin  6971  ixpiinm  6972  infmoti  7332  acfun  7527  exmidontriimlem1  7541  exmidontriimlem3  7543  ccfunen  7594  cc2  7597  cc4f  7599  cc4n  7601  cauappcvgprlemladdrl  7988  axcaucvglemres  8230  axpre-suploc  8233  dfinfre  9247  suprzclex  9694  supinfneg  9945  infsupneg  9946  infssuzex  10615  hashfibc  11232  cvg1nlemcau  11694  cvg1nlemres  11695  rexfiuz  11699  recvguniq  11705  resqrexlemglsq  11732  resqrexlemsqa  11734  resqrexlemex  11735  clim0  11995  mertenslem2  12247  bezoutlemmain  12719  ballotfilem7  13223  ennnfoneleminc  13246  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemr  13258  ctinfom  13263  isnsg2  13956  isbasis2g  15036  tgval2  15042  ntreq0  15123  lmres  15239  eltx  15250  suplociccreex  15615  lgseisenlem2  16070  vtxd0nedgbfi  16420  decidi  16693  nninfsellemqall  16919  nninfomni  16923  trirec0xor  16955