Theorem raleqbidv 2684

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  ∀wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  rspc2vd  3125  ofrfval  6090  fmpox  6200  tfrlemi1  6332  supeq123d  6989  cvg1nlemcau  10988  cvg1nlemres  10989  cau3lem  11118  fsum2dlemstep  11437  fisumcom2  11441  fprod2dlemstep  11625  fprodcom2fi  11629  pcfac  12342  ptex  12707  prdsex  12712  ismgm  12770  mgm1  12783  grpidvalg  12786  issgrp  12803  sgrp1  12810  ismnddef  12813  ismndd  12832  mndpropd  12835  mnd1  12841  ismhm  12847  isgrp  12877  grppropd  12887  isgrpd2e  12890  grp1  12970  isnsg  13055  nmznsg  13066  cmnpropd  13091  iscmnd  13094  dfur2g  13138  issrg  13141  issrgid  13157  isring  13176  iscrng2  13191  ringideu  13193  isringid  13201  ringpropd  13210  ring1  13229  oppr0g  13244  oppr1g  13245  islring  13326  istopg  13430  restbasg  13599  cnfval  13625  cnpfval  13626  txbas  13689  limccl  14059  sscoll2  14660