![]() |
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 3349 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1658 ∀wral 3116 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 |
This theorem is referenced by: ralrab2 3594 ralprg 4452 raltpg 4454 ralxp 5495 f12dfv 6783 f13dfv 6784 ralrnmpt2 7034 ovmptss 7521 ixpfi2 8532 dffi3 8605 dfoi 8684 fseqenlem1 9159 kmlem12 9297 fzprval 12694 fztpval 12695 hashbc 13525 2prm 15776 prmreclem2 15991 xpsfrnel 16575 xpsle 16593 gsumwspan 17736 sgrp2rid2 17766 psgnunilem3 18266 pmtrsn 18289 ply1coe 20025 cply1coe0bi 20029 islinds2 20518 m2cpminvid2lem 20928 basdif0 21127 ordtbaslem 21362 ptbasfi 21754 ptcnplem 21794 ptrescn 21812 flftg 22169 ust0 22392 minveclem1 23591 minveclem3b 23595 minveclem6 23601 iblcnlem1 23952 ellimc2 24039 ftalem3 25213 dchreq 25395 pntlem3 25710 istrkg2ld 25771 istrkg3ld 25772 elntg2 26283 lfuhgr1v0e 26550 cplgr0 26722 wlkp1lem8 26980 usgr2pthlem 27064 pthdlem1 27067 pthd 27070 crctcshwlkn0 27119 2wlkdlem4 27256 2wlkdlem5 27257 2pthdlem1 27258 2wlkdlem10 27263 rusgrnumwwlkl1 27296 0ewlk 27489 0wlk 27491 wlk2v2elem2 27531 3wlkdlem4 27537 3wlkdlem5 27538 3pthdlem1 27539 3wlkdlem10 27544 minvecolem1 28284 minvecolem5 28291 minvecolem6 28292 cdj3lem3b 29853 prsiga 30738 hfext 32828 filnetlem4 32913 relowlssretop 33755 relowlpssretop 33756 elghomOLD 34227 iscrngo2 34337 refrelcoss3 34760 tendoset 36833 fnwe2lem2 38463 eliuniincex 40106 eliincex 40107 uzub 40452 liminflelimsuplem 40801 xlimbr 40847 subsaliuncl 41366 isomushgr 42543 rrx2linest 43295 |
Copyright terms: Public domain | W3C validator |