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  6169  fmpox  6288  tfrlemi1  6420  supeq123d  7095  acneq  7316  cvg1nlemcau  11328  cvg1nlemres  11329  cau3lem  11458  fsum2dlemstep  11778  fisumcom2  11782  fprod2dlemstep  11966  fprodcom2fi  11970  pcfac  12706  ptex  13129  prdsex  13134  prdsval  13138  ismgm  13222  mgm1  13235  grpidvalg  13238  gsumress  13260  issgrp  13268  sgrp1  13276  sgrppropd  13278  ismnddef  13283  ismndd  13302  mndpropd  13305  mnd1  13320  ismhm  13326  mhmex  13327  resmhm  13352  isgrp  13371  grppropd  13382  isgrpd2e  13385  grp1  13471  isnsg  13571  nmznsg  13582  isghm  13612  cmnpropd  13664  iscmnd  13667  isrng  13729  rngpropd  13750  dfur2g  13757  issrg  13760  issrgid  13776  isring  13795  iscrng2  13810  ringideu  13812  isringid  13820  ringpropd  13833  ring1  13854  oppr0g  13876  oppr1g  13877  isrhm2d  13960  rhmopp  13971  islring  13987  rrgval  14057  isdomn  14064  opprdomnbg  14069  islmod  14086  islmodd  14088  lmodprop2d  14143  lsssetm  14151  islidlm  14274  rnglidlmmgm  14291  rnglidlmsgrp  14292  mplvalcoe  14485  istopg  14504  restbasg  14673  cnfval  14699  cnpfval  14700  txbas  14763  limccl  15164  sscoll2  15961