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  6315  fmpox  6440  tfrlemi1  6608  supeq123d  7337  acneq  7564  cvg1nlemcau  11771  cvg1nlemres  11772  cau3lem  11902  fsum2dlemstep  12225  fisumcom2  12229  fprod2dlemstep  12413  fprodcom2fi  12417  pcfac  13157  ptex  13676  ismgm  13735  mgm1  13748  grpidvalg  13751  gzsumress  13770  issgrp  13776  sgrp1  13784  sgrppropd  13786  ismnddef  13789  ismndd  13808  mndpropd  13811  mnd1  13820  ismhm  13826  mhmex  13827  resmhm  13852  isgrp  13869  grppropd  13880  isgrpd2e  13883  grp1  13969  isnsg  14063  nmznsg  14074  isghm  14104  cmnpropd  14187  iscmnd  14190  prdsex  14278  prdsval  14279  isrng  14339  rngpropd  14360  dfur2g  14372  issrg  14375  issrgid  14391  isring  14410  iscrng2  14425  ringideu  14427  isringid  14436  ringpropd  14449  ring1  14470  oppr0g  14495  oppr1g  14496  isrhm2d  14580  rhmopp  14591  islring  14607  opprlring  14612  rrgval  14678  isdomn  14686  opprdomnbg  14691  islmod  14735  islmodd  14737  lmodprop2d  14793  lsssetm  14801  islidlm  14924  rnglidlmmgm  14941  rnglidlmsgrp  14942  isassa  15110  isassad  15119  assapropd  15122  istopg  15242  restbasg  15411  cnfval  15437  cnpfval  15438  txbas  15501  limccl  15902  iswlk  16786  isclwwlk  16857  sscoll2  17236