Theorem ralbii 2536

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

Syntax hints:   ↔ wb 105  ⊤wtru 1396  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-ral 2513

This theorem is referenced by:  2ralbii  2538  ralinexa  2557  r3al  2574  r19.26-2  2660  r19.26-3  2661  ralbiim  2665  r19.28av  2667  ralnex2  2670  ralrot3  2696  cbvral2vw  2776  cbvral2v  2778  cbvral3v  2780  sbralie  2783  ralcom4  2822  reu8  2999  2reuswapdc  3007  r19.12sn  3732  eqsnm  3833  uni0b  3913  uni0c  3914  ssint  3939  iuniin  3975  iuneq2  3981  iunss  4006  ssiinf  4015  iinab  4027  iindif2m  4033  iinin2m  4034  iinuniss  4048  sspwuni  4050  iinpw  4056  dftr3  4186  trint  4197  bnd2  4257  reusv3  4551  reg2exmidlema  4626  setindel  4630  ordsoexmid  4654  zfregfr  4666  tfi  4674  tfis2f  4676  ssrel2  4809  reliun  4840  xpiindim  4859  ralxpf  4868  dfse2  5101  rninxp  5172  dminxp  5173  cnviinm  5270  cnvpom  5271  cnvsom  5272  dffun9  5347  funco  5358  funcnv3  5383  fncnv  5387  funimaexglem  5404  fnres  5440  fnopabg  5447  mptfng  5449  fintm  5513  f1ompt  5788  idref  5886  dff13f  5900  foov  6158  tfr1onlemaccex  6500  tfrcllembxssdm  6508  tfrcllemaccex  6513  oacl  6614  ixpeq2  6867  ixpin  6878  ixpiinm  6879  infmoti  7206  acfun  7400  exmidontriimlem1  7414  exmidontriimlem3  7416  ccfunen  7461  cc2  7464  cc4f  7466  cc4n  7468  cauappcvgprlemladdrl  7855  axcaucvglemres  8097  axpre-suploc  8100  dfinfre  9114  suprzclex  9556  supinfneg  9802  infsupneg  9803  infssuzex  10465  cvg1nlemcau  11510  cvg1nlemres  11511  rexfiuz  11515  recvguniq  11521  resqrexlemglsq  11548  resqrexlemsqa  11550  resqrexlemex  11551  clim0  11811  mertenslem2  12062  bezoutlemmain  12534  ennnfoneleminc  12997  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemr  13009  ctinfom  13014  isnsg2  13755  isbasis2g  14734  tgval2  14740  ntreq0  14821  lmres  14937  eltx  14948  suplociccreex  15313  lgseisenlem2  15765  decidi  16214  nninfsellemqall  16441  nninfomni  16445  trirec0xor  16473