Theorem ralbii 2513

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

Syntax hints:   ↔ wb 105  ⊤wtru 1374  ∀wral 2485

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-ral 2490

This theorem is referenced by:  2ralbii  2515  ralinexa  2534  r3al  2551  r19.26-2  2636  r19.26-3  2637  ralbiim  2641  r19.28av  2643  ralnex2  2646  ralrot3  2672  cbvral2vw  2750  cbvral2v  2752  cbvral3v  2754  sbralie  2757  ralcom4  2796  reu8  2973  2reuswapdc  2981  r19.12sn  3703  eqsnm  3801  uni0b  3880  uni0c  3881  ssint  3906  iuniin  3942  iuneq2  3948  iunss  3973  ssiinf  3982  iinab  3994  iindif2m  4000  iinin2m  4001  iinuniss  4015  sspwuni  4017  iinpw  4023  dftr3  4153  trint  4164  bnd2  4224  reusv3  4514  reg2exmidlema  4589  setindel  4593  ordsoexmid  4617  zfregfr  4629  tfi  4637  tfis2f  4639  ssrel2  4772  reliun  4803  xpiindim  4822  ralxpf  4831  dfse2  5063  rninxp  5134  dminxp  5135  cnviinm  5232  cnvpom  5233  cnvsom  5234  dffun9  5308  funco  5319  funcnv3  5344  fncnv  5348  funimaexglem  5365  fnres  5401  fnopabg  5408  mptfng  5410  fintm  5472  f1ompt  5743  idref  5837  dff13f  5851  foov  6105  tfr1onlemaccex  6446  tfrcllembxssdm  6454  tfrcllemaccex  6459  oacl  6558  ixpeq2  6811  ixpin  6822  ixpiinm  6823  infmoti  7144  acfun  7334  exmidontriimlem1  7348  exmidontriimlem3  7350  ccfunen  7391  cc2  7394  cc4f  7396  cc4n  7398  cauappcvgprlemladdrl  7785  axcaucvglemres  8027  axpre-suploc  8030  dfinfre  9044  suprzclex  9486  supinfneg  9731  infsupneg  9732  infssuzex  10393  cvg1nlemcau  11365  cvg1nlemres  11366  rexfiuz  11370  recvguniq  11376  resqrexlemglsq  11403  resqrexlemsqa  11405  resqrexlemex  11406  clim0  11666  mertenslem2  11917  bezoutlemmain  12389  ennnfoneleminc  12852  ennnfonelemex  12855  ennnfonelemhom  12856  ennnfonelemr  12864  ctinfom  12869  isnsg2  13609  isbasis2g  14587  tgval2  14593  ntreq0  14674  lmres  14790  eltx  14801  suplociccreex  15166  lgseisenlem2  15618  decidi  15865  nninfsellemqall  16087  nninfomni  16091  trirec0xor  16119