Theorem raleq 1324

Description: Equality theorem for restricted universal quantifier.

Assertion

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

Distinct variable group(s):   x,A   x,B

Proof of Theorem raleq

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

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092  ∀wral 1201

This theorem is referenced by:  raleqd 1327  sbralie 1439  inteq 1968  iineq1 2004  supeq1 2155  fri 2170  tfis 2245  tfinds 2401  cbvfo 2923  isoeq4 2928  f1oweOLD 2944  tfrlem1 2949  tfrlem3 2951  tfrlem12 2960  bnd2 3549  aceq3lem 3555  aceq5lem4 3561  aceq5 3563  ac4c 3572  ac5 3573  kmlem1 3580  kmlem9 3588  kmlem11 3590  kmlem12 3591  zornlem6 3608  zornlem7 3609  zorn 3611  cfval 3701  ocvalt 5161

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-9 799  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099  df-ral 1205

metamath.org