| 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 form). (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 3178 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
| 3 | 2 | ralbidv 3178 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3062 |
| This theorem is referenced by: 3ralbidv 3224 6ralbidv 3226 cbvral3vw 3243 cbvral6vw 3245 cbvral3v 3370 rspc6v 3643 ralxpxfr2d 3646 poeq1 5595 soeq1 5613 isoeq1 7337 isoeq2 7338 isoeq3 7339 fnmpoovd 8112 xpord3inddlem 8179 smoeq 8390 xpf1o 9179 nqereu 10969 dedekind 11424 dedekindle 11425 seqcaopr2 14079 wrd2ind 14761 addcn2 15630 mulcn2 15632 mreexexd 17691 catlid 17726 catrid 17727 isfunc 17909 funcres2b 17942 isfull 17957 isfth 17961 fullres2c 17986 isnat 17995 evlfcl 18267 uncfcurf 18284 isprs 18342 isdrs 18347 ispos 18360 istos 18463 isdlat 18567 ismgmhm 18709 issubmgm 18715 sgrp1 18742 ismhm 18798 issubm 18816 sgrp2nmndlem4 18941 isnsg 19173 isghm 19233 isghmOLD 19234 isga 19309 pmtrdifwrdel 19503 sylow2blem2 19639 efglem 19734 efgi 19737 efgredlemb 19764 efgred 19766 frgpuplem 19790 iscmn 19807 ring1 20307 isirred 20419 rnghmval 20440 isrnghm 20441 islmod 20862 lmodlema 20863 lssset 20931 islssd 20933 islmhm 21026 islmhm2 21037 isobs 21740 dmatel 22499 dmatmulcl 22506 scmateALT 22518 mdetunilem3 22620 mdetunilem4 22621 mdetunilem9 22626 cpmatel 22717 chpscmat 22848 hausnei2 23361 dfconn2 23427 llyeq 23478 nllyeq 23479 isucn2 24288 iducn 24292 ispsmet 24314 ismet 24333 isxmet 24334 metucn 24584 ngptgp 24649 nlmvscnlem1 24707 xmetdcn2 24859 addcnlem 24886 elcncf 24915 ipcnlem1 25279 cfili 25302 c1lip1 26036 aalioulem5 26378 aalioulem6 26379 aaliou 26380 aaliou2 26382 aaliou2b 26383 ulmcau 26438 ulmdvlem3 26445 cxpcn3lem 26790 mpodvdsmulf1o 27237 dvdsmulf1o 27239 chpdifbndlem2 27598 pntrsumbnd2 27611 addsprop 28009 negsprop 28067 istrkgb 28463 axtgsegcon 28472 axtg5seg 28473 axtgpasch 28475 axtgeucl 28480 iscgrg 28520 isismt 28542 isperp2 28723 f1otrg 28879 axcontlem10 28988 axcontlem12 28990 iscusgredg 29440 isgrpo 30516 isablo 30565 vacn 30713 smcnlem 30716 lnoval 30771 islno 30772 isphg 30836 ajmoi 30877 ajval 30880 adjmo 31851 elcnop 31876 ellnop 31877 elunop 31891 elhmop 31892 elcnfn 31901 ellnfn 31902 adjeu 31908 adjval 31909 adj1 31952 adjeq 31954 cnlnadjlem9 32094 cnlnadjeu 32097 cnlnssadj 32099 isst 32232 ishst 32233 cdj1i 32452 cdj3i 32460 resspos 32956 resstos 32957 ismnt 32973 mgcval 32977 isomnd 33078 isslmd 33208 slmdlema 33209 isorng 33329 prmidlval 33465 isprmidl 33466 isrprm 33545 qqhucn 33993 ismntop 34027 axtgupdim2ALTV 34683 txpconn 35237 nn0prpw 36324 heicant 37662 equivbnd 37797 isismty 37808 heibor1lem 37816 iccbnd 37847 isass 37853 elghomlem1OLD 37892 elghomlem2OLD 37893 isrngohom 37972 iscom2 38002 pridlval 38040 ispridl 38041 isdmn3 38081 inecmo 38356 islfl 39061 isopos 39181 psubspset 39746 islaut 40085 ispautN 40101 ltrnset 40120 isltrn 40121 istrnN 40159 istendo 40762 sticksstones1 42147 sticksstones2 42148 sticksstones3 42149 sticksstones8 42154 sticksstones10 42156 sticksstones11 42157 sticksstones12a 42158 sticksstones15 42162 sn-isghm 42683 clsk1independent 44059 relpeq1 44965 relpeq2 44966 relpeq3 44967 sprsymrelfolem2 47480 sprsymrelfo 47484 reuopreuprim 47513 dmatALTbasel 48319 lindslinindsimp2 48380 lmod1 48409 isnrm4 48828 iscnrm4 48851 isuplem 48936 isthinc 49069 thincciso 49102 thinccisod 49103 |
| Copyright terms: Public domain | W3C validator |