Theorem raleqbidv 2744

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 2734	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜓))
3		raleqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	ralbidv 2530	. 2 ⊢ (𝜑 → (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ∀wral 2508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  rspc2vd  3193  ofrfval  6236  fmpox  6357  tfrlemi1  6489  supeq123d  7174  acneq  7400  cvg1nlemcau  11516  cvg1nlemres  11517  cau3lem  11646  fsum2dlemstep  11966  fisumcom2  11970  fprod2dlemstep  12154  fprodcom2fi  12158  pcfac  12894  ptex  13318  prdsex  13323  prdsval  13327  ismgm  13411  mgm1  13424  grpidvalg  13427  gsumress  13449  issgrp  13457  sgrp1  13465  sgrppropd  13467  ismnddef  13472  ismndd  13491  mndpropd  13494  mnd1  13509  ismhm  13515  mhmex  13516  resmhm  13541  isgrp  13560  grppropd  13571  isgrpd2e  13574  grp1  13660  isnsg  13760  nmznsg  13771  isghm  13801  cmnpropd  13853  iscmnd  13856  isrng  13918  rngpropd  13939  dfur2g  13946  issrg  13949  issrgid  13965  isring  13984  iscrng2  13999  ringideu  14001  isringid  14009  ringpropd  14022  ring1  14043  oppr0g  14065  oppr1g  14066  isrhm2d  14150  rhmopp  14161  islring  14177  rrgval  14247  isdomn  14254  opprdomnbg  14259  islmod  14276  islmodd  14278  lmodprop2d  14333  lsssetm  14341  islidlm  14464  rnglidlmmgm  14481  rnglidlmsgrp  14482  mplvalcoe  14675  istopg  14694  restbasg  14863  cnfval  14889  cnpfval  14890  txbas  14953  limccl  15354  iswlk  16095  isclwwlk  16163  sscoll2  16460