Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > raleqbidv | Structured version Visualization version GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) Remove usage of ax-10 2141, ax-11 2158, and ax-12 2175 and reduce distinct variable conditions. (Revised by Steven Nguyen, 30-Apr-2023.) |
Ref | Expression |
---|---|
raleqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
raleqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
raleqbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidv.1 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 1 | eleq2d 2819 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
3 | raleqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | imbi12d 348 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
5 | 4 | ralbidv2 3109 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 ∈ wcel 2110 ∀wral 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2706 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-cleq 2726 df-clel 2812 df-ral 3059 |
This theorem is referenced by: rspc2vd 3853 f12dfv 7073 f13dfv 7074 knatar 7155 ofrfvalg 7465 fmpox 7826 ovmptss 7850 frrlem4 8019 marypha1lem 9038 supeq123d 9055 oieq1 9117 acneq 9640 isfin1a 9889 fpwwe2cbv 10227 fpwwe2lem2 10229 fpwwecbv 10241 fpwwelem 10242 eltskg 10347 elgrug 10389 cau3lem 14901 rlim 15039 ello1 15059 elo1 15070 caurcvg2 15224 caucvgb 15226 fsum2dlem 15315 fsumcom2 15319 fprod2dlem 15523 fprodcom2 15527 pcfac 16433 vdwpc 16514 rami 16549 prmgaplem7 16591 prdsval 16932 ismre 17065 isacs2 17128 acsfiel 17129 iscat 17147 iscatd 17148 catidex 17149 catideu 17150 cidfval 17151 cidval 17152 catlid 17158 catrid 17159 comfeq 17181 catpropd 17184 monfval 17209 issubc 17313 fullsubc 17328 isfunc 17342 funcpropd 17379 isfull 17389 isfth 17393 fthpropd 17400 natfval 17425 initoval 17471 termoval 17472 isposd 17802 lubfval 17828 glbfval 17841 ismgm 18087 issstrmgm 18097 grpidval 18105 gsumvalx 18120 gsumpropd 18122 gsumress 18126 issgrp 18136 ismnddef 18147 ismndd 18167 mndpropd 18170 ismhm 18192 resmhm 18219 isgrp 18343 grppropd 18354 isgrpd2e 18358 isnsg 18543 nmznsg 18556 isghm 18594 isga 18657 subgga 18666 gsmsymgrfix 18792 gsmsymgreq 18796 gexval 18939 ispgp 18953 isslw 18969 sylow2blem2 18982 efgval 19079 efgi 19081 efgsdm 19092 cmnpropd 19152 iscmnd 19155 submcmn2 19196 gsumzaddlem 19278 dmdprd 19357 dprdcntz 19367 issrg 19494 isring 19538 ringpropd 19572 isirred 19689 sdrgacs 19817 abvfval 19826 abvpropd 19850 islmod 19875 islmodd 19877 lmodprop2d 19933 lssset 19942 islmhm 20036 reslmhm 20061 lmhmpropd 20082 islbs 20085 rrgval 20297 isdomn 20304 psgndiflemA 20535 isphl 20562 islindf 20746 islindf2 20748 lsslindf 20764 isassa 20790 isassad 20798 assapropd 20803 ltbval 20972 opsrval 20975 dmatval 21361 dmatcrng 21371 scmatcrng 21390 cpmat 21578 istopg 21764 restbas 22027 ordtrest2 22073 cnfval 22102 cnpfval 22103 ist0 22189 ist1 22190 ishaus 22191 iscnrm 22192 isnrm 22204 ist0-2 22213 ishaus2 22220 nrmsep3 22224 iscmp 22257 is1stc 22310 isptfin 22385 islocfin 22386 kgenval 22404 kgencn2 22426 txbas 22436 ptval 22439 dfac14 22487 isfil 22716 isufil 22772 isufl 22782 flfcntr 22912 ucnval 23146 iscusp 23168 prdsxmslem2 23399 tngngp3 23526 isnlm 23545 nmofval 23584 lebnumii 23835 iscau4 24148 iscmet 24153 iscmet3lem1 24160 iscmet3 24162 equivcmet 24186 ulmcaulem 25258 ulmcau 25259 fsumdvdscom 26039 dchrisumlem3 26344 pntibndlem2 26444 pntibnd 26446 pntlemp 26463 ostth2lem2 26487 trgcgrg 26578 tgcgr4 26594 isismt 26597 nbgr2vtx1edg 27410 nbuhgr2vtx1edgb 27412 uvtxval 27447 uvtxel 27448 uvtxel1 27456 uvtxusgrel 27463 cusgredg 27484 cplgr3v 27495 cplgrop 27497 usgredgsscusgredg 27519 isrgr 27619 isewlk 27662 iswlk 27670 iswwlks 27892 wlkiswwlks2 27931 isclwwlk 28039 clwlkclwwlklem1 28054 isconngr 28244 isconngr1 28245 isfrgr 28315 frgr1v 28326 nfrgr2v 28327 frgr3v 28330 1vwmgr 28331 3vfriswmgr 28333 3cyclfrgrrn1 28340 n4cyclfrgr 28346 isplig 28529 gidval 28565 vciOLD 28614 isvclem 28630 isnvlem 28663 lnoval 28805 ajfval 28862 isphg 28870 minvecolem3 28929 htth 28971 ressprs 30932 mntoval 30951 mgcoval 30955 isslmd 31146 resv1r 31227 prmidlval 31298 mxidlval 31319 isufd 31349 rprmval 31350 iscref 31480 ordtrest2NEW 31559 fmcncfil 31567 issiga 31764 isrnsiga 31765 isldsys 31808 ismeas 31851 carsgval 31954 issibf 31984 sitgfval 31992 signstfvneq0 32235 istrkg2d 32330 ispconn 32870 issconn 32873 txpconn 32879 cvxpconn 32889 cvmscbv 32905 iscvm 32906 cvmsdisj 32917 cvmsss2 32921 snmlval 32978 elmrsubrn 33167 ismfs 33196 mclsval 33210 on2ind 33522 on3ind 33523 madebdayim 33764 no2indslem 33805 no3inds 33809 fwddifnval 34159 bj-ismoore 34968 pibp19 35279 pibp21 35280 poimirlem28 35499 cover2g 35567 seqpo 35599 incsequz2 35601 caushft 35613 ismtyval 35652 isass 35698 isexid 35699 elghomlem1OLD 35737 isrngo 35749 isrngod 35750 isgrpda 35807 rngohomval 35816 iscom2 35847 idlval 35865 pridlval 35885 maxidlval 35891 elrefrels3 36330 elcnvrefrels3 36343 eleqvrels3 36400 lflset 36767 islfld 36770 isopos 36888 isoml 36946 isatl 37007 iscvlat 37031 ishlat1 37060 psubspset 37452 lautset 37790 pautsetN 37806 ldilfset 37816 ltrnfset 37825 dilfsetN 37860 trnfsetN 37863 trnsetN 37864 trlfset 37868 tendofset 38466 tendoset 38467 dihffval 38938 lpolsetN 39190 hdmapfval 39535 hgmapfval 39594 aomclem8 40541 islnm 40557 clsk1independent 41285 gneispace2 41371 gneispaceel2 41383 gneispacess2 41385 ioodvbdlimc1lem1 43101 ioodvbdlimc1lem2 43102 ioodvbdlimc2lem 43104 issal 43484 ismea 43618 isome 43661 iccpartiltu 44501 iccelpart 44512 isomgr 44902 isupwlk 44925 mgmpropd 44956 ismgmd 44957 ismgmhm 44964 resmgmhm 44979 iscllaw 45010 iscomlaw 45011 isasslaw 45013 isrng 45061 c0snmgmhm 45099 zlidlring 45113 uzlidlring 45114 dmatALTval 45368 islininds 45414 lindslinindsimp2 45431 ldepsnlinc 45476 elbigo 45524 iscnrm3r 45869 isprsd 45876 lubeldm2d 45879 glbeldm2d 45880 isthincd2lem2 45944 isthincd 45945 |
Copyright terms: Public domain | W3C validator |