Theorem ralbii 2511

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

Syntax hints:   ↔ wb 105  ⊤wtru 1373  ∀wral 2483

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-ral 2488

This theorem is referenced by:  2ralbii  2513  ralinexa  2532  r3al  2549  r19.26-2  2634  r19.26-3  2635  ralbiim  2639  r19.28av  2641  ralnex2  2644  ralrot3  2670  cbvral2vw  2748  cbvral2v  2750  cbvral3v  2752  sbralie  2755  ralcom4  2793  reu8  2968  2reuswapdc  2976  r19.12sn  3698  eqsnm  3795  uni0b  3874  uni0c  3875  ssint  3900  iuniin  3936  iuneq2  3942  iunss  3967  ssiinf  3976  iinab  3988  iindif2m  3994  iinin2m  3995  iinuniss  4009  sspwuni  4011  iinpw  4017  dftr3  4145  trint  4156  bnd2  4216  reusv3  4506  reg2exmidlema  4581  setindel  4585  ordsoexmid  4609  zfregfr  4621  tfi  4629  tfis2f  4631  ssrel2  4764  reliun  4795  xpiindim  4814  ralxpf  4823  dfse2  5054  rninxp  5125  dminxp  5126  cnviinm  5223  cnvpom  5224  cnvsom  5225  dffun9  5299  funco  5310  funcnv3  5335  fncnv  5339  funimaexglem  5356  fnres  5391  fnopabg  5398  mptfng  5400  fintm  5460  f1ompt  5730  idref  5824  dff13f  5838  foov  6092  tfr1onlemaccex  6433  tfrcllembxssdm  6441  tfrcllemaccex  6446  oacl  6545  ixpeq2  6798  ixpin  6809  ixpiinm  6810  infmoti  7129  acfun  7318  exmidontriimlem1  7332  exmidontriimlem3  7334  ccfunen  7375  cc2  7378  cc4f  7380  cc4n  7382  cauappcvgprlemladdrl  7769  axcaucvglemres  8011  axpre-suploc  8014  dfinfre  9028  suprzclex  9470  supinfneg  9715  infsupneg  9716  infssuzex  10374  cvg1nlemcau  11266  cvg1nlemres  11267  rexfiuz  11271  recvguniq  11277  resqrexlemglsq  11304  resqrexlemsqa  11306  resqrexlemex  11307  clim0  11567  mertenslem2  11818  bezoutlemmain  12290  ennnfoneleminc  12753  ennnfonelemex  12756  ennnfonelemhom  12757  ennnfonelemr  12765  ctinfom  12770  isnsg2  13510  isbasis2g  14488  tgval2  14494  ntreq0  14575  lmres  14691  eltx  14702  suplociccreex  15067  lgseisenlem2  15519  decidi  15693  nninfsellemqall  15914  nninfomni  15918  trirec0xor  15946