![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > raleqbidv | Unicode version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 6-Nov-2007.) |
Ref | Expression |
---|---|
raleqbidv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
raleqbidv.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
raleqbidv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleqbidv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | raleqdv 2692 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | raleqbidv.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ralbidv 2490 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 188 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 |
This theorem is referenced by: rspc2vd 3140 ofrfval 6110 fmpox 6220 tfrlemi1 6352 supeq123d 7015 cvg1nlemcau 11020 cvg1nlemres 11021 cau3lem 11150 fsum2dlemstep 11469 fisumcom2 11473 fprod2dlemstep 11657 fprodcom2fi 11661 pcfac 12377 ptex 12762 prdsex 12767 ismgm 12826 mgm1 12839 grpidvalg 12842 issgrp 12859 sgrp1 12867 sgrppropd 12869 ismnddef 12872 ismndd 12891 mndpropd 12894 mnd1 12900 ismhm 12906 mhmex 12907 resmhm 12932 isgrp 12944 grppropd 12955 isgrpd2e 12958 grp1 13043 isnsg 13134 nmznsg 13145 isghm 13175 cmnpropd 13227 iscmnd 13230 isrng 13281 rngpropd 13302 dfur2g 13309 issrg 13312 issrgid 13328 isring 13347 iscrng2 13362 ringideu 13364 isringid 13372 ringpropd 13385 ring1 13404 oppr0g 13424 oppr1g 13425 isrhm2d 13508 rhmopp 13519 islring 13532 islmod 13600 islmodd 13602 lmodprop2d 13657 lsssetm 13665 islidlm 13788 rnglidlmmgm 13805 rnglidlmsgrp 13806 istopg 13936 restbasg 14105 cnfval 14131 cnpfval 14132 txbas 14195 limccl 14565 sscoll2 15177 |
Copyright terms: Public domain | W3C validator |