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 3407 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 = wceq 1537 ∀wral 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2816 df-clel 2895 df-ral 3145 |
This theorem is referenced by: ralrab2 3692 ralprgf 4632 raltpg 4636 ralxp 5714 f12dfv 7032 f13dfv 7033 ralrnmpo 7291 ovmptss 7790 ixpfi2 8824 dffi3 8897 dfoi 8977 fseqenlem1 9452 kmlem12 9589 fzprval 12971 fztpval 12972 hashbc 13814 2prm 16038 prmreclem2 16255 xpsfrnel 16837 xpsle 16854 gsumwspan 18013 sgrp2rid2 18093 psgnunilem3 18626 pmtrsn 18649 ply1coe 20466 cply1coe0bi 20470 islinds2 20959 m2cpminvid2lem 21364 basdif0 21563 ordtbaslem 21798 ptbasfi 22191 ptcnplem 22231 ptrescn 22249 flftg 22606 ust0 22830 minveclem1 24029 minveclem3b 24033 minveclem6 24039 iblcnlem1 24390 ellimc2 24477 ftalem3 25654 dchreq 25836 pntlem3 26187 istrkg2ld 26248 istrkg3ld 26249 tgcgr4 26319 elntg2 26773 lfuhgr1v0e 27038 cplgr0 27209 wlkp1lem8 27464 usgr2pthlem 27546 pthdlem1 27549 pthd 27552 crctcshwlkn0 27601 2wlkdlem4 27709 2wlkdlem5 27710 2pthdlem1 27711 2wlkdlem10 27716 rusgrnumwwlkl1 27749 0ewlk 27895 0wlk 27897 wlk2v2elem2 27937 3wlkdlem4 27943 3wlkdlem5 27944 3pthdlem1 27945 3wlkdlem10 27950 minvecolem1 28653 minvecolem5 28660 minvecolem6 28661 cdj3lem3b 30219 prsiga 31392 hfext 33646 filnetlem4 33731 relowlssretop 34646 relowlpssretop 34647 elghomOLD 35167 iscrngo2 35277 refrelcoss3 35705 tendoset 37897 fnwe2lem2 39658 eliuniincex 41382 eliincex 41383 uzub 41712 liminflelimsuplem 42063 xlimbr 42115 subsaliuncl 42648 isomushgr 43998 rrx2pnecoorneor 44709 rrx2linest 44736 |
Copyright terms: Public domain | W3C validator |