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  7332  acneq  7559  cvg1nlemcau  11766  cvg1nlemres  11767  cau3lem  11897  fsum2dlemstep  12220  fisumcom2  12224  fprod2dlemstep  12408  fprodcom2fi  12412  pcfac  13152  ptex  13671  ismgm  13730  mgm1  13743  grpidvalg  13746  gzsumress  13765  issgrp  13771  sgrp1  13779  sgrppropd  13781  ismnddef  13784  ismndd  13803  mndpropd  13806  mnd1  13815  ismhm  13821  mhmex  13822  resmhm  13847  isgrp  13864  grppropd  13875  isgrpd2e  13878  grp1  13964  isnsg  14058  nmznsg  14069  isghm  14099  cmnpropd  14182  iscmnd  14185  prdsex  14256  prdsval  14257  isrng  14317  rngpropd  14338  dfur2g  14350  issrg  14353  issrgid  14369  isring  14388  iscrng2  14403  ringideu  14405  isringid  14414  ringpropd  14427  ring1  14448  oppr0g  14471  oppr1g  14472  isrhm2d  14556  rhmopp  14567  islring  14583  opprlring  14588  rrgval  14654  isdomn  14662  opprdomnbg  14667  islmod  14711  islmodd  14713  lmodprop2d  14769  lsssetm  14777  islidlm  14900  rnglidlmmgm  14917  rnglidlmsgrp  14918  isassa  15086  isassad  15095  assapropd  15098  mplvalcoe  15172  istopg  15191  restbasg  15360  cnfval  15386  cnpfval  15387  txbas  15450  limccl  15851  iswlk  16730  isclwwlk  16801  sscoll2  17180