raleq - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > raleq		Unicode version

Theorem raleq 2749

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

**Assertion**
Ref	Expression
raleq

(

)

**Proof of Theorem raleq**
Step	Hyp	Ref	Expression
1		nfcv 2392	. 2
2		nfcv 2392	. 2
3	1, 2	raleqf 2745	1

Colors of variables: wff set class

This proof depends on syntax axioms:

wi 4

wb 105

wceq 1402

wral 2528

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-ext 2220

This proof depends on definitions: df-bi 117 df-tru 1405 df-nf 1514 df-sb 1816 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533

This theorem is used by: raleqi 2753 raleqdv 2755 raleqbi1dv 2761 sbralie 2804 inteq 3973 iineq1 4026 bnd2 4310 frforeq2 4490 weeq2 4502 ordeq 4517 reg2exmid 4683 reg3exmid 4727 omsinds 4769 fncnv 5447 funimaexglem 5464 isoeq4 6010 acexmidlemv 6083 tfrlem1 6579 tfr0dm 6593 tfrlemisucaccv 6596 tfrlemi1 6603 tfrlemi14d 6604 tfrexlem 6605 tfr1onlemsucaccv 6612 tfr1onlemaccex 6619 tfr1onlemres 6620 tfrcllemsucaccv 6625 tfrcllembxssdm 6627 tfrcllemaccex 6632 tfrcllemres 6633 tfrcldm 6634 ixpeq1 6991 ac6sfi 7202 fimax2gtri 7206 dcfi 7315 supeq1 7327 supeq2 7330 nnnninfeq2 7470 isomni 7477 ismkv 7494 iswomni 7506 acneq 7559 papeq2 7611 tapeq2 7620 sup3exmid 9290 rexanuz 11770 rexfiuz 11771 fimaxre2 12010 fiidxsupcl 12012 modfsummod 12244 mhmpropd 13826 isghm 14099 cntzval 14147 iscmn 14180 srgideu 14360 dfrhm2 14545 cnprcl2k 15398 ispsmet 15515 ismet 15536 isxmet 15537 cncfval 15764 dvcn 15892 setindis 17159 bdsetindis 17161 strcoll2 17175 strcollnfALT 17178