Theorem ralbii 2380

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

Syntax hints:   ↔ wb 103  ⊤wtru 1288  ∀wral 2355

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462

This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-ral 2360

This theorem is referenced by:  2ralbii  2382  ralinexa  2401  r3al  2416  r19.26-2  2494  r19.26-3  2495  ralbiim  2499  r19.28av  2501  cbvral2v  2594  cbvral3v  2596  sbralie  2599  ralcom4  2635  reu8  2802  2reuswapdc  2808  r19.12sn  3493  eqsnm  3584  uni0b  3663  uni0c  3664  ssint  3689  iuniin  3725  iuneq2  3731  iunss  3756  ssiinf  3764  iinab  3776  iindif2m  3782  iinin2m  3783  iinuniss  3795  sspwuni  3797  iinpw  3800  dftr3  3917  trint  3928  bnd2  3985  reusv3  4258  reg2exmidlema  4325  setindel  4329  ordsoexmid  4353  zfregfr  4364  tfi  4372  tfis2f  4374  ssrel2  4498  reliun  4528  xpiindim  4543  ralxpf  4552  dfse2  4774  rninxp  4842  dminxp  4843  cnviinm  4940  cnvpom  4941  cnvsom  4942  dffun9  5011  funco  5021  funcnv3  5043  fncnv  5047  funimaexglem  5064  fnres  5097  fnopabg  5104  mptfng  5106  fintm  5161  f1ompt  5415  idref  5499  dff13f  5512  foov  5750  tfr1onlemaccex  6069  tfrcllembxssdm  6077  tfrcllemaccex  6082  oacl  6177  infmoti  6670  cauappcvgprlemladdrl  7163  axcaucvglemres  7381  dfinfre  8355  suprzclex  8780  supinfneg  9018  infsupneg  9019  cvg1nlemcau  10334  cvg1nlemres  10335  rexfiuz  10339  recvguniq  10345  resqrexlemglsq  10372  resqrexlemsqa  10374  resqrexlemex  10375  clim0  10589  infssuzex  10870  bezoutlemmain  10912  decidi  11183  nninfsellemqall  11395  nninfomni  11399