![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > raleqbi1dv | Structured version Visualization version GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.) |
Ref | Expression |
---|---|
raleqbi1dv.1 | ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
raleqbi1dv | ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
2 | raleqbi1dv.1 | . 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | raleqbidv 3335 | 1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1507 ∀wral 3082 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2765 df-clel 2840 df-ral 3087 |
This theorem is referenced by: raleq 3339 isoeq4 6890 wfrlem1 7750 wfrlem4 7754 wfrlem4OLD 7755 wfrlem15 7766 smo11 7798 dffi2 8674 inficl 8676 dffi3 8682 dfom3 8896 aceq1 9329 dfac5lem4 9338 kmlem1 9362 kmlem10 9371 kmlem13 9374 kmlem14 9375 cofsmo 9481 infpssrlem4 9518 axdc3lem2 9663 elwina 9898 elina 9899 iswun 9916 eltskg 9962 elgrug 10004 elnp 10199 elnpi 10200 dfnn2 11446 dfnn3 11447 dfuzi 11879 coprmprod 15851 coprmproddvds 15853 ismri 16750 isprs 17388 isdrs 17392 ispos 17405 istos 17493 pospropd 17592 isipodrs 17619 isdlat 17651 mhmpropd 17799 issubm 17805 subgacs 18088 nsgacs 18089 isghm 18119 ghmeql 18142 iscmn 18663 dfrhm2 19182 islss 19418 lssacs 19451 lmhmeql 19539 islbs 19560 lbsextlem1 19642 lbsextlem3 19644 lbsextlem4 19645 isobs 20556 mat0dimcrng 20773 istopg 21197 isbasisg 21249 basis2 21253 eltg2 21260 iscldtop 21397 neipeltop 21431 isreg 21634 regsep 21636 isnrm 21637 islly 21770 isnlly 21771 llyi 21776 nllyi 21777 islly2 21786 cldllycmp 21797 isfbas 22131 fbssfi 22139 isust 22505 elutop 22535 ustuqtop 22548 utopsnneip 22550 ispsmet 22607 ismet 22626 isxmet 22627 metrest 22827 cncfval 23189 fmcfil 23568 iscfil3 23569 caucfil 23579 iscmet3 23589 cfilres 23592 minveclem3 23725 wilthlem2 25338 wilthlem3 25339 wilth 25340 dfconngr1 27707 isconngr 27708 1conngr 27713 isplig 28020 isgrpo 28041 isablo 28090 disjabrex 30088 disjabrexf 30089 isomnd 30398 isorng 30507 isrnsigaOLD 30973 isrnsiga 30974 isldsys 31017 isros 31029 issros 31036 bnj1286 31897 bnj1452 31930 kur14lem9 32006 cvmscbv 32050 cvmsi 32057 cvmsval 32058 frrlem1 32584 frrlem13 32596 neibastop1 33168 neibastop2lem 33169 neibastop2 33170 rdgssun 34036 isbnd 34448 ismndo2 34542 rngomndo 34603 isidl 34682 ispsubsp 36274 isnacs 38641 mzpclval 38662 elmzpcl 38663 mgmhmpropd 43360 issubmgm 43364 rnghmval 43466 zrrnghm 43492 |
Copyright terms: Public domain | W3C validator |