Theorem ralbii 2439

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

Syntax hints:   ↔ wb 104  ⊤wtru 1332  ∀wral 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-ral 2419

This theorem is referenced by:  2ralbii  2441  ralinexa  2460  r3al  2475  r19.26-2  2559  r19.26-3  2560  ralbiim  2564  r19.28av  2566  ralnex2  2569  cbvral2v  2660  cbvral3v  2662  sbralie  2665  ralcom4  2703  reu8  2875  2reuswapdc  2883  r19.12sn  3584  eqsnm  3677  uni0b  3756  uni0c  3757  ssint  3782  iuniin  3818  iuneq2  3824  iunss  3849  ssiinf  3857  iinab  3869  iindif2m  3875  iinin2m  3876  iinuniss  3890  sspwuni  3892  iinpw  3898  dftr3  4025  trint  4036  bnd2  4092  reusv3  4376  reg2exmidlema  4444  setindel  4448  ordsoexmid  4472  zfregfr  4483  tfi  4491  tfis2f  4493  ssrel2  4624  reliun  4655  xpiindim  4671  ralxpf  4680  dfse2  4907  rninxp  4977  dminxp  4978  cnviinm  5075  cnvpom  5076  cnvsom  5077  dffun9  5147  funco  5158  funcnv3  5180  fncnv  5184  funimaexglem  5201  fnres  5234  fnopabg  5241  mptfng  5243  fintm  5303  f1ompt  5564  idref  5651  dff13f  5664  foov  5910  tfr1onlemaccex  6238  tfrcllembxssdm  6246  tfrcllemaccex  6251  oacl  6349  ixpeq2  6599  ixpin  6610  ixpiinm  6611  infmoti  6908  acfun  7056  ccfunen  7072  cauappcvgprlemladdrl  7458  axcaucvglemres  7700  axpre-suploc  7703  dfinfre  8707  suprzclex  9142  supinfneg  9383  infsupneg  9384  cvg1nlemcau  10749  cvg1nlemres  10750  rexfiuz  10754  recvguniq  10760  resqrexlemglsq  10787  resqrexlemsqa  10789  resqrexlemex  10790  clim0  11047  mertenslem2  11298  infssuzex  11631  bezoutlemmain  11675  ennnfoneleminc  11913  ennnfonelemex  11916  ennnfonelemhom  11917  ennnfonelemr  11925  ctinfom  11930  isbasis2g  12201  tgval2  12209  ntreq0  12290  lmres  12406  eltx  12417  suplociccreex  12760  decidi  12991  nninfsellemqall  13200  nninfomni  13204