Theorem ralbii 2548

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

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

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 2525

This theorem is referenced by:  2ralbii  2550  ralinexa  2569  r3al  2586  r19.26-2  2672  r19.26-3  2673  ralbiim  2677  r19.28av  2679  ralnex2  2682  ralrot3  2708  cbvral2vw  2788  cbvral2v  2790  cbvral3v  2792  sbralie  2795  ralcom4  2835  reu8  3012  2reuswapdc  3020  r19.12sn  3754  eqsnm  3858  uni0b  3938  uni0c  3939  ssint  3964  iuniin  4000  iuneq2  4006  iunss  4031  ssiinf  4040  iinab  4052  iindif2m  4058  iinin2m  4059  iinuniss  4073  sspwuni  4075  iinpw  4081  dftr3  4211  trint  4222  bnd2  4285  reusv3  4580  reg2exmidlema  4655  setindel  4659  ordsoexmid  4683  zfregfr  4695  tfi  4703  tfis2f  4705  ssrel2  4839  reliun  4872  xpiindim  4891  ralxpf  4900  dfse2  5134  rninxp  5205  dminxp  5206  cnviinm  5303  cnvpom  5304  cnvsom  5305  dffun9  5380  funco  5391  funcnv3  5417  fncnv  5421  funimaexglem  5438  fnres  5474  fnopabg  5481  mptfng  5483  fintm  5551  f1ompt  5827  idref  5928  dff13f  5942  foov  6200  tfr1onlemaccex  6578  tfrcllembxssdm  6586  tfrcllemaccex  6591  oacl  6692  ixpeq2  6946  ixpin  6957  ixpiinm  6958  infmoti  7318  acfun  7513  exmidontriimlem1  7527  exmidontriimlem3  7529  ccfunen  7577  cc2  7580  cc4f  7582  cc4n  7584  cauappcvgprlemladdrl  7971  axcaucvglemres  8213  axpre-suploc  8216  dfinfre  9229  suprzclex  9675  supinfneg  9926  infsupneg  9927  infssuzex  10592  hashfibc  11203  cvg1nlemcau  11665  cvg1nlemres  11666  rexfiuz  11670  recvguniq  11676  resqrexlemglsq  11703  resqrexlemsqa  11705  resqrexlemex  11706  clim0  11966  mertenslem2  12218  bezoutlemmain  12690  ennnfoneleminc  13154  ennnfonelemex  13157  ennnfonelemhom  13158  ennnfonelemr  13166  ctinfom  13171  isnsg2  13912  isbasis2g  14902  tgval2  14908  ntreq0  14989  lmres  15105  eltx  15116  suplociccreex  15481  lgseisenlem2  15936  vtxd0nedgbfi  16286  decidi  16559  nninfsellemqall  16785  nninfomni  16789  trirec0xor  16821