![]() |
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 3311 | . 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-ral 3051 df-rex 3060 |
This theorem is referenced by: ralrab2 3690 ralprgf 4698 ralprg 4700 raltpg 4704 ralxp 5844 f12dfv 7282 f13dfv 7283 ralrnmpo 7560 ovmptss 8098 ixpfi2 9376 dffi3 9456 dfoi 9536 ssttrcl 9740 fseqenlem1 10049 kmlem12 10186 fzprval 13597 fztpval 13598 hashbc 14448 2prm 16666 prmreclem2 16889 xpsfrnel 17547 xpsle 17564 gsumwspan 18806 sgrp2rid2 18886 psgnunilem3 19463 pmtrsn 19486 islinds2 21764 ply1coe 22242 cply1coe0bi 22246 m2cpminvid2lem 22700 basdif0 22900 ordtbaslem 23136 ptbasfi 23529 ptcnplem 23569 ptrescn 23587 flftg 23944 ust0 24168 minveclem1 25396 minveclem3b 25400 minveclem6 25406 iblcnlem1 25761 ellimc2 25850 ftalem3 27052 dchreq 27236 pntlem3 27587 negsbdaylem 28014 precsexlem9 28163 istrkg2ld 28336 istrkg3ld 28337 tgcgr4 28407 elntg2 28868 lfuhgr1v0e 29139 cplgr0 29310 wlkp1lem8 29566 usgr2pthlem 29649 pthdlem1 29652 pthd 29655 crctcshwlkn0 29704 2wlkdlem4 29811 2wlkdlem5 29812 2pthdlem1 29813 2wlkdlem10 29818 rusgrnumwwlkl1 29851 0ewlk 29996 0wlk 29998 wlk2v2elem2 30038 3wlkdlem4 30044 3wlkdlem5 30045 3pthdlem1 30046 3wlkdlem10 30051 minvecolem1 30756 minvecolem5 30763 minvecolem6 30764 cdj3lem3b 32322 prsiga 33881 hfext 35910 filnetlem4 35996 relowlssretop 36973 relowlpssretop 36974 elghomOLD 37491 iscrngo2 37601 refrelcoss3 38065 tendoset 40362 fnwe2lem2 42617 nadd1suc 42963 eliuniincex 44615 eliincex 44616 uzub 44951 liminflelimsuplem 45301 xlimbr 45353 subsaliuncl 45884 gricushgr 47369 rrx2pnecoorneor 47974 rrx2linest 48001 |
Copyright terms: Public domain | W3C validator |