![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > raleqi | Structured version Visualization version GIF version |
Description: Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
raleq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
raleqi | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | raleq 3322 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1653 ∀wral 3090 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2778 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-cleq 2793 df-clel 2796 df-nfc 2931 df-ral 3095 |
This theorem is referenced by: ralrab2 3567 ralprg 4425 raltpg 4427 ralxp 5468 f12dfv 6758 f13dfv 6759 ralrnmpt2 7010 ovmptss 7496 ixpfi2 8507 dffi3 8580 dfoi 8659 fseqenlem1 9134 kmlem12 9272 fzprval 12654 fztpval 12655 hashbc 13485 2prm 15738 prmreclem2 15953 xpsfrnel 16537 xpsle 16555 gsumwspan 17698 sgrp2rid2 17728 psgnunilem3 18228 pmtrsn 18251 ply1coe 19987 cply1coe0bi 19991 islinds2 20476 m2cpminvid2lem 20886 basdif0 21085 ordtbaslem 21320 ptbasfi 21712 ptcnplem 21752 ptrescn 21770 flftg 22127 ust0 22350 minveclem1 23533 minveclem3b 23537 minveclem6 23543 iblcnlem1 23894 ellimc2 23981 ftalem3 25152 dchreq 25334 pntlem3 25649 istrkg2ld 25710 istrkg3ld 25711 lfuhgr1v0e 26487 cplgr0 26674 wlkp1lem8 26932 usgr2pthlem 27016 pthdlem1 27019 pthd 27022 crctcshwlkn0 27071 2wlkdlem4 27216 2wlkdlem5 27217 2pthdlem1 27218 2wlkdlem10 27223 rusgrnumwwlkl1 27258 0ewlk 27457 0wlk 27459 wlk2v2elem2 27499 3wlkdlem4 27505 3wlkdlem5 27506 3pthdlem1 27507 3wlkdlem10 27512 minvecolem1 28254 minvecolem5 28261 minvecolem6 28262 cdj3lem3b 29823 prsiga 30709 hfext 32802 filnetlem4 32887 relowlssretop 33708 relowlpssretop 33709 elghomOLD 34172 iscrngo2 34282 refrelcoss3 34706 tendoset 36779 fnwe2lem2 38401 eliuniincex 40045 eliincex 40046 uzub 40396 liminflelimsuplem 40746 xlimbr 40792 subsaliuncl 41314 isomushgr 42491 |
Copyright terms: Public domain | W3C validator |