Theorem ralbii 2483

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

Syntax hints:   ↔ wb 105  ⊤wtru 1354  ∀wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-ral 2460

This theorem is referenced by:  2ralbii  2485  ralinexa  2504  r3al  2521  r19.26-2  2606  r19.26-3  2607  ralbiim  2611  r19.28av  2613  ralnex2  2616  ralrot3  2642  cbvral2vw  2715  cbvral2v  2717  cbvral3v  2719  sbralie  2722  ralcom4  2760  reu8  2934  2reuswapdc  2942  r19.12sn  3659  eqsnm  3756  uni0b  3835  uni0c  3836  ssint  3861  iuniin  3897  iuneq2  3903  iunss  3928  ssiinf  3937  iinab  3949  iindif2m  3955  iinin2m  3956  iinuniss  3970  sspwuni  3972  iinpw  3978  dftr3  4106  trint  4117  bnd2  4174  reusv3  4461  reg2exmidlema  4534  setindel  4538  ordsoexmid  4562  zfregfr  4574  tfi  4582  tfis2f  4584  ssrel2  4717  reliun  4748  xpiindim  4765  ralxpf  4774  dfse2  5002  rninxp  5073  dminxp  5074  cnviinm  5171  cnvpom  5172  cnvsom  5173  dffun9  5246  funco  5257  funcnv3  5279  fncnv  5283  funimaexglem  5300  fnres  5333  fnopabg  5340  mptfng  5342  fintm  5402  f1ompt  5668  idref  5758  dff13f  5771  foov  6021  tfr1onlemaccex  6349  tfrcllembxssdm  6357  tfrcllemaccex  6362  oacl  6461  ixpeq2  6712  ixpin  6723  ixpiinm  6724  infmoti  7027  acfun  7206  exmidontriimlem1  7220  exmidontriimlem3  7222  ccfunen  7263  cc2  7266  cc4f  7268  cc4n  7270  cauappcvgprlemladdrl  7656  axcaucvglemres  7898  axpre-suploc  7901  dfinfre  8913  suprzclex  9351  supinfneg  9595  infsupneg  9596  cvg1nlemcau  10993  cvg1nlemres  10994  rexfiuz  10998  recvguniq  11004  resqrexlemglsq  11031  resqrexlemsqa  11033  resqrexlemex  11034  clim0  11293  mertenslem2  11544  infssuzex  11950  bezoutlemmain  11999  ennnfoneleminc  12412  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemr  12424  ctinfom  12429  isnsg2  13063  isbasis2g  13548  tgval2  13554  ntreq0  13635  lmres  13751  eltx  13762  suplociccreex  14105  lgseisenlem2  14454  decidi  14550  nninfsellemqall  14767  nninfomni  14771  trirec0xor  14796