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 3113 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | ralbidv 3113 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3065 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ral 3070 |
This theorem is referenced by: cbvral3vw 3399 cbvral3v 3402 ralxpxfr2d 3577 poeq1 5507 soeq1 5525 isoeq1 7197 isoeq2 7198 isoeq3 7199 fnmpoovd 7936 smoeq 8190 xpf1o 8935 nqereu 10694 dedekind 11147 dedekindle 11148 seqcaopr2 13768 wrd2ind 14445 addcn2 15312 mulcn2 15314 mreexexd 17366 catlid 17401 catrid 17402 isfunc 17588 funcres2b 17621 isfull 17635 isfth 17639 fullres2c 17664 isnat 17672 evlfcl 17949 uncfcurf 17966 isprs 18024 isdrs 18028 ispos 18041 istos 18145 isdlat 18249 sgrp1 18393 ismhm 18441 issubm 18451 sgrp2nmndlem4 18576 isnsg 18792 isghm 18843 isga 18906 pmtrdifwrdel 19102 sylow2blem2 19235 efglem 19331 efgi 19334 efgredlemb 19361 efgred 19363 frgpuplem 19387 iscmn 19403 ring1 19850 isirred 19950 islmod 20136 lmodlema 20137 lssset 20204 islssd 20206 islmhm 20298 islmhm2 20309 isobs 20936 dmatel 21651 dmatmulcl 21658 scmateALT 21670 mdetunilem3 21772 mdetunilem4 21773 mdetunilem9 21778 cpmatel 21869 chpscmat 22000 hausnei2 22513 dfconn2 22579 llyeq 22630 nllyeq 22631 isucn2 23440 iducn 23444 ispsmet 23466 ismet 23485 isxmet 23486 metucn 23736 ngptgp 23801 nlmvscnlem1 23859 xmetdcn2 24009 addcnlem 24036 elcncf 24061 ipcnlem1 24418 cfili 24441 c1lip1 25170 aalioulem5 25505 aalioulem6 25506 aaliou 25507 aaliou2 25509 aaliou2b 25510 ulmcau 25563 ulmdvlem3 25570 cxpcn3lem 25909 dvdsmulf1o 26352 chpdifbndlem2 26711 pntrsumbnd2 26724 istrkgb 26825 axtgsegcon 26834 axtg5seg 26835 axtgpasch 26837 axtgeucl 26842 iscgrg 26882 isismt 26904 isperp2 27085 f1otrg 27241 axcontlem10 27350 axcontlem12 27352 iscusgredg 27799 isgrpo 28868 isablo 28917 vacn 29065 smcnlem 29068 lnoval 29123 islno 29124 isphg 29188 ajmoi 29229 ajval 29232 adjmo 30203 elcnop 30228 ellnop 30229 elunop 30243 elhmop 30244 elcnfn 30253 ellnfn 30254 adjeu 30260 adjval 30261 adj1 30304 adjeq 30306 cnlnadjlem9 30446 cnlnadjeu 30449 cnlnssadj 30451 isst 30584 ishst 30585 cdj1i 30804 cdj3i 30812 resspos 31253 resstos 31254 ismnt 31270 mgcval 31274 isomnd 31336 isslmd 31464 slmdlema 31465 isorng 31507 prmidlval 31621 isprmidl 31622 isrprm 31674 qqhucn 31951 ismntop 31985 axtgupdim2ALTV 32657 txpconn 33203 xpord3ind 33809 nn0prpw 34521 heicant 35821 equivbnd 35957 isismty 35968 heibor1lem 35976 iccbnd 36007 isass 36013 elghomlem1OLD 36052 elghomlem2OLD 36053 isrngohom 36132 iscom2 36162 pridlval 36200 ispridl 36201 isdmn3 36241 inecmo 36494 islfl 37081 isopos 37201 psubspset 37765 islaut 38104 ispautN 38120 ltrnset 38139 isltrn 38140 istrnN 38178 istendo 38781 sticksstones1 40109 sticksstones2 40110 sticksstones3 40111 sticksstones8 40116 sticksstones10 40118 sticksstones11 40119 sticksstones12a 40120 sticksstones15 40124 clsk1independent 41663 sprsymrelfolem2 44956 sprsymrelfo 44960 reuopreuprim 44989 ismgmhm 45348 issubmgm 45354 rnghmval 45460 isrnghm 45461 lidlmsgrp 45495 lidlrng 45496 dmatALTbasel 45754 lindslinindsimp2 45815 lmod1 45844 isnrm4 46235 iscnrm4 46259 isthinc 46313 thincciso 46341 |
Copyright terms: Public domain | W3C validator |