Theorem raleqbidv 2765

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.)

Hypotheses

Ref	Expression
raleqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
raleqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
raleqbidv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem raleqbidv

Step	Hyp	Ref	Expression
1		raleqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	raleqdv 2755	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 2550	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  rspc2vd  3216  ofrfval  6311  fmpox  6436  tfrlemi1  6603  supeq123d  7331  acneq  7558  cvg1nlemcau  11764  cvg1nlemres  11765  cau3lem  11895  fsum2dlemstep  12217  fisumcom2  12221  fprod2dlemstep  12405  fprodcom2fi  12409  pcfac  13149  ptex  13667  ismgm  13726  mgm1  13739  grpidvalg  13742  gzsumress  13761  issgrp  13767  sgrp1  13775  sgrppropd  13777  ismnddef  13780  ismndd  13799  mndpropd  13802  mnd1  13811  ismhm  13817  mhmex  13818  resmhm  13843  isgrp  13860  grppropd  13871  isgrpd2e  13874  grp1  13960  isnsg  14054  nmznsg  14065  isghm  14095  cmnpropd  14147  iscmnd  14150  prdsex  14221  prdsval  14222  isrng  14282  rngpropd  14303  dfur2g  14315  issrg  14318  issrgid  14334  isring  14353  iscrng2  14368  ringideu  14370  isringid  14379  ringpropd  14392  ring1  14413  oppr0g  14436  oppr1g  14437  isrhm2d  14521  rhmopp  14532  islring  14548  opprlring  14553  rrgval  14619  isdomn  14627  opprdomnbg  14632  islmod  14676  islmodd  14678  lmodprop2d  14734  lsssetm  14742  islidlm  14865  rnglidlmmgm  14882  rnglidlmsgrp  14883  isassa  15051  isassad  15060  assapropd  15063  mplvalcoe  15130  istopg  15149  restbasg  15318  cnfval  15344  cnpfval  15345  txbas  15408  limccl  15809  iswlk  16662  isclwwlk  16733  sscoll2  17112