Theorem ralbii 2539

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

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

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 2516

This theorem is referenced by:  2ralbii  2541  ralinexa  2560  r3al  2577  r19.26-2  2663  r19.26-3  2664  ralbiim  2668  r19.28av  2670  ralnex2  2673  ralrot3  2699  cbvral2vw  2779  cbvral2v  2781  cbvral3v  2783  sbralie  2786  ralcom4  2826  reu8  3003  2reuswapdc  3011  r19.12sn  3739  eqsnm  3843  uni0b  3923  uni0c  3924  ssint  3949  iuniin  3985  iuneq2  3991  iunss  4016  ssiinf  4025  iinab  4037  iindif2m  4043  iinin2m  4044  iinuniss  4058  sspwuni  4060  iinpw  4066  dftr3  4196  trint  4207  bnd2  4269  reusv3  4563  reg2exmidlema  4638  setindel  4642  ordsoexmid  4666  zfregfr  4678  tfi  4686  tfis2f  4688  ssrel2  4822  reliun  4854  xpiindim  4873  ralxpf  4882  dfse2  5116  rninxp  5187  dminxp  5188  cnviinm  5285  cnvpom  5286  cnvsom  5287  dffun9  5362  funco  5373  funcnv3  5399  fncnv  5403  funimaexglem  5420  fnres  5456  fnopabg  5463  mptfng  5465  fintm  5530  f1ompt  5806  idref  5907  dff13f  5921  foov  6179  tfr1onlemaccex  6557  tfrcllembxssdm  6565  tfrcllemaccex  6570  oacl  6671  ixpeq2  6924  ixpin  6935  ixpiinm  6936  infmoti  7270  acfun  7465  exmidontriimlem1  7479  exmidontriimlem3  7481  ccfunen  7526  cc2  7529  cc4f  7531  cc4n  7533  cauappcvgprlemladdrl  7920  axcaucvglemres  8162  axpre-suploc  8165  dfinfre  9178  suprzclex  9622  supinfneg  9873  infsupneg  9874  infssuzex  10539  cvg1nlemcau  11607  cvg1nlemres  11608  rexfiuz  11612  recvguniq  11618  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  clim0  11908  mertenslem2  12160  bezoutlemmain  12632  ennnfoneleminc  13095  ennnfonelemex  13098  ennnfonelemhom  13099  ennnfonelemr  13107  ctinfom  13112  isnsg2  13853  isbasis2g  14839  tgval2  14845  ntreq0  14926  lmres  15042  eltx  15053  suplociccreex  15418  lgseisenlem2  15873  vtxd0nedgbfi  16223  decidi  16496  nninfsellemqall  16724  nninfomni  16728  trirec0xor  16760