Theorem raleqbidv 2718

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ∀wral 2484

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489

This theorem is referenced by:  rspc2vd  3162  ofrfval  6167  fmpox  6286  tfrlemi1  6418  supeq123d  7093  acneq  7314  cvg1nlemcau  11295  cvg1nlemres  11296  cau3lem  11425  fsum2dlemstep  11745  fisumcom2  11749  fprod2dlemstep  11933  fprodcom2fi  11937  pcfac  12673  ptex  13096  prdsex  13101  prdsval  13105  ismgm  13189  mgm1  13202  grpidvalg  13205  gsumress  13227  issgrp  13235  sgrp1  13243  sgrppropd  13245  ismnddef  13250  ismndd  13269  mndpropd  13272  mnd1  13287  ismhm  13293  mhmex  13294  resmhm  13319  isgrp  13338  grppropd  13349  isgrpd2e  13352  grp1  13438  isnsg  13538  nmznsg  13549  isghm  13579  cmnpropd  13631  iscmnd  13634  isrng  13696  rngpropd  13717  dfur2g  13724  issrg  13727  issrgid  13743  isring  13762  iscrng2  13777  ringideu  13779  isringid  13787  ringpropd  13800  ring1  13821  oppr0g  13843  oppr1g  13844  isrhm2d  13927  rhmopp  13938  islring  13954  rrgval  14024  isdomn  14031  opprdomnbg  14036  islmod  14053  islmodd  14055  lmodprop2d  14110  lsssetm  14118  islidlm  14241  rnglidlmmgm  14258  rnglidlmsgrp  14259  mplvalcoe  14452  istopg  14471  restbasg  14640  cnfval  14666  cnpfval  14667  txbas  14730  limccl  15131  sscoll2  15924