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 4312 frforeq2 4492 weeq2 4504 ordeq 4519 reg2exmid 4685 reg3exmid 4729 omsinds 4771 fncnv 5450 funimaexglem 5467 isoeq4 6013 acexmidlemv 6086 tfrlem1 6583 tfr0dm 6597 tfrlemisucaccv 6600 tfrlemi1 6607 tfrlemi14d 6608 tfrexlem 6609 tfr1onlemsucaccv 6616 tfr1onlemaccex 6623 tfr1onlemres 6624 tfrcllemsucaccv 6629 tfrcllembxssdm 6631 tfrcllemaccex 6636 tfrcllemres 6637 tfrcldm 6638 ixpeq1 6995 ac6sfi 7206 fimax2gtri 7210 dcfi 7320 supeq1 7332 supeq2 7335 nnnninfeq2 7475 isomni 7482 ismkv 7499 iswomni 7511 acneq 7564 papeq2 7616 tapeq2 7625 sup3exmid 9295 rexanuz 11776 rexfiuz 11777 fimaxre2 12016 fiidxsupcl 12018 modfsummod 12250 mhmpropd 13832 isghm 14105 cntzval 14153 iscmn 14186 srgideu 14383 dfrhm2 14570 cnprcl2k 15432 ispsmet 15549 ismet 15570 isxmet 15571 cncfval 15798 dvcn 15926 setindis 17198 bdsetindis 17200 strcoll2 17214 strcollnfALT 17217