Theorem raleqbidv 2685

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 2679	. 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  3126  ofrfval  6091  fmpox  6201  tfrlemi1  6333  supeq123d  6990  cvg1nlemcau  10993  cvg1nlemres  10994  cau3lem  11123  fsum2dlemstep  11442  fisumcom2  11446  fprod2dlemstep  11630  fprodcom2fi  11634  pcfac  12348  ptex  12713  prdsex  12718  ismgm  12776  mgm1  12789  grpidvalg  12792  issgrp  12809  sgrp1  12816  ismnddef  12819  ismndd  12838  mndpropd  12841  mnd1  12847  ismhm  12853  isgrp  12883  grppropd  12893  isgrpd2e  12896  grp1  12976  isnsg  13062  nmznsg  13073  cmnpropd  13098  iscmnd  13101  dfur2g  13145  issrg  13148  issrgid  13164  isring  13183  iscrng2  13198  ringideu  13200  isringid  13208  ringpropd  13217  ring1  13236  oppr0g  13251  oppr1g  13252  islring  13333  islmod  13381  islmodd  13383  lmodprop2d  13438  istopg  13502  restbasg  13671  cnfval  13697  cnpfval  13698  txbas  13761  limccl  14131  sscoll2  14743