![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbidv | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.) (Revised by Szymon Jaroszewicz, 16-Mar-2007.) |
Ref | Expression |
---|---|
2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2ralbidv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | ralbidv 3015 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 3015 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∀wral 2941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ral 2946 |
This theorem is referenced by: cbvral3v 3211 ralxpxfr2d 3358 poeq1 5067 soeq1 5083 isoeq1 6607 isoeq2 6608 isoeq3 6609 fnmpt2ovd 7297 smoeq 7492 xpf1o 8163 nqereu 9789 dedekind 10238 dedekindle 10239 seqcaopr2 12877 wrd2ind 13523 addcn2 14368 mulcn2 14370 mreexexd 16355 mreexexdOLD 16356 catlid 16391 catrid 16392 isfunc 16571 funcres2b 16604 isfull 16617 isfth 16621 fullres2c 16646 isnat 16654 evlfcl 16909 uncfcurf 16926 isprs 16977 isdrs 16981 ispos 16994 istos 17082 isdlat 17240 sgrp1 17340 ismhm 17384 issubm 17394 sgrp2nmndlem4 17462 isnsg 17670 isghm 17707 isga 17770 pmtrdifwrdel 17951 sylow2blem2 18082 efglem 18175 efgi 18178 efgredlemb 18205 efgred 18207 frgpuplem 18231 iscmn 18246 ring1 18648 isirred 18745 islmod 18915 lmodlema 18916 lssset 18982 islssd 18984 islmhm 19075 islmhm2 19086 isobs 20112 dmatel 20347 dmatmulcl 20354 scmateALT 20366 mdetunilem3 20468 mdetunilem4 20469 mdetunilem9 20474 cpmatel 20564 chpscmat 20695 hausnei2 21205 dfconn2 21270 llyeq 21321 nllyeq 21322 isucn2 22130 iducn 22134 ispsmet 22156 ismet 22175 isxmet 22176 metucn 22423 ngptgp 22487 nlmvscnlem1 22537 xmetdcn2 22687 addcnlem 22714 elcncf 22739 ipcnlem1 23090 cfili 23112 c1lip1 23805 aalioulem5 24136 aalioulem6 24137 aaliou 24138 aaliou2 24140 aaliou2b 24141 ulmcau 24194 ulmdvlem3 24201 cxpcn3lem 24533 dvdsmulf1o 24965 chpdifbndlem2 25288 pntrsumbnd2 25301 istrkgb 25399 axtgsegcon 25408 axtg5seg 25409 axtgpasch 25411 axtgeucl 25416 iscgrg 25452 isismt 25474 isperp2 25655 f1otrg 25796 axcontlem10 25898 axcontlem12 25900 isgrpo 27479 isablo 27528 vacn 27677 smcnlem 27680 lnoval 27735 islno 27736 isphg 27800 ajmoi 27842 ajval 27845 adjmo 28819 elcnop 28844 ellnop 28845 elunop 28859 elhmop 28860 elcnfn 28869 ellnfn 28870 adjeu 28876 adjval 28877 adj1 28920 adjeq 28922 cnlnadjlem9 29062 cnlnadjeu 29065 cnlnssadj 29067 isst 29200 ishst 29201 cdj1i 29420 cdj3i 29428 resspos 29787 resstos 29788 isomnd 29829 isslmd 29883 slmdlema 29884 isorng 29927 qqhucn 30164 ismntop 30198 axtgupdim2OLD 30874 txpconn 31340 nn0prpw 32443 heicant 33574 equivbnd 33719 isismty 33730 heibor1lem 33738 iccbnd 33769 isass 33775 elghomlem1OLD 33814 elghomlem2OLD 33815 isrngohom 33894 iscom2 33924 pridlval 33962 ispridl 33963 isdmn3 34003 inecmo 34260 islfl 34665 isopos 34785 psubspset 35348 islaut 35687 ispautN 35703 ltrnset 35722 isltrn 35723 istrnN 35762 istendo 36365 clsk1independent 38661 sprsymrelfolem2 42068 sprsymrelfo 42072 ismgmhm 42108 issubmgm 42114 isrnghm 42217 lidlmsgrp 42251 lidlrng 42252 dmatALTbasel 42516 lindslinindsimp2 42577 lmod1 42606 |
Copyright terms: Public domain | W3C validator |