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 qualifier. (Contributed by Paul Chapman, 22-Jun-2011.) |
Ref | Expression |
---|---|
raleq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
raleqi | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | raleq 3115 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 |
This theorem is referenced by: ralrab2 3339 ralprg 4181 raltpg 4183 ralxp 5185 f12dfv 6429 f13dfv 6430 ralrnmpt2 6673 ovmptss 7145 ixpfi2 8147 dffi3 8220 dfoi 8299 fseqenlem1 8730 kmlem12 8866 fzprval 12271 fztpval 12272 hashbc 13094 2prm 15243 prmreclem2 15459 xpsfrnel 16046 xpsle 16064 gsumwspan 17206 sgrp2rid2 17236 psgnunilem3 17739 pmtrsn 17762 ply1coe 19487 cply1coe0bi 19491 islinds2 19971 m2cpminvid2lem 20378 basdif0 20568 ordtbaslem 20802 ptbasfi 21194 ptcnplem 21234 ptrescn 21252 flftg 21610 ust0 21833 minveclem1 23003 minveclem3b 23007 minveclem6 23013 iblcnlem1 23360 ellimc2 23447 ftalem3 24601 dchreq 24783 pntlem3 25098 istrkg2ld 25159 istrkg3ld 25160 cusgra3v 25993 cusgrares 26001 0wlk 26075 0trl 26076 wlkntrllem2 26090 usgrcyclnl2 26169 3v3e3cycl1 26172 4cycl4v4e 26194 4cycl4dv4e 26196 rusgranumwlkl1 26474 minvecolem1 27114 minvecolem5 27121 minvecolem6 27122 cdj3lem3b 28683 prsiga 29521 hfext 31460 filnetlem4 31546 relowlssretop 32387 relowlpssretop 32388 elghomOLD 32856 iscrngo2 32966 tendoset 35065 fnwe2lem2 36639 eliuniincex 38323 eliincex 38324 subsaliuncl 39252 lfuhgr1v0e 40480 cplgr0 40647 1wlkp1lem8 40889 usgr2pthlem 40969 pthdlem1 40972 pthd 40975 crctcsh1wlkn0 41024 21wlkdlem4 41135 21wlkdlem5 41136 2pthdlem1 41137 21wlkdlem10 41142 rusgrnumwwlkl1 41172 0ewlk 41282 01wlk 41284 1wlk2v2elem2 41323 31wlkdlem4 41329 31wlkdlem5 41330 3pthdlem1 41331 31wlkdlem10 41336 |
Copyright terms: Public domain | W3C validator |