Theorem raleq1 1789

Description: Equality theorem for restricted universal quantifier.

Assertion

Ref	Expression
raleq1	⊢ (A = B → (∀x ∈ A φ ↔ ∀x ∈ B φ))

Distinct variable groups:   x,A   x,B

Proof of Theorem raleq1

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 ⊢ (y ∈ A → ∀x y ∈ A)
2		ax-17 973	. 2 ⊢ (y ∈ B → ∀x y ∈ B)
3	1, 2	raleq1f 1786	1 ⊢ (A = B → (∀x ∈ A φ ↔ ∀x ∈ B φ))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 958   ∈ wcel 960  ∀wral 1648

This theorem is referenced by:  raleq1d 1792  raleqd 1794  sbralie 1944  inteq 2540  iineq1 2580  fri 2924  tfis 3133  tfinds 3167  fncnv 3567  cbvfo 3891  isoeq4 3896  f1oweALT 3912  tfrlem1 3917  tfrlem3 3919  tfrlem12 3928  ixpeq1 4359  unifiOLD 4570  supeq1 4584  bnd2 4734  aceq3lem 4742  aceq5lem4 4748  aceq5 4750  ac4c 4761  ac5 4762  kmlem1 4775  kmlem10 4784  kmlem12 4786  kmlem13 4787  zorn2lem7 4804  zorn2 4806  unidomg 4819  cfval 4918  xrsupsslem 6078  xrinfmsslem 6079  xrsupss 6080  xrinfmss 6081  cau4i 6918  cau5 6919  clmnns 7084  isumnn0nn 7207  infcvglem3 7223  cncfval 7264  acdc3lem 7487  acdc3 7488  acdc2lem1 7489  acdc2 7491  acdc5lem1 7492  acdc5 7494  acdclem 7495  acdc 7496  basgen2t 7638  cnfval 7753  cnpfval 7754  ismet 7795  dfms2 7796  ismsg 7797  msflem 7800  metreslem 7819  isgrp 8038  isabl 8097  ringi 8138  minveclem30 8570  spwval2 8649  spwpr2 8654  spwval 8655  spwnex 8657  ocvalt 9148  cdj3lem3b 10362  elghom 10379  homeofval 10502

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475  df-ral 1652

Copyright terms: Public domain