Definition df-ral 2533

Description: Define restricted universal quantification. Special case of Definition 4.15(3) of [TakeutiZaring] p. 22. (Contributed by NM, 19-Aug-1993.)

Assertion

Ref	Expression
df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3		cA	. . 3 class A
4	1, 2, 3	wral 2528	. 2 wff A. x e. A ph
5	2	cv 1401	. . . . 5 class x
6	5, 3	wcel 2209	. . . 4 wff x e. A
7	6, 1	wi 4	. . 3 wff ( x e. A -> ph )
8	7, 2	wal 1400	. 2 wff A. x ( x e. A -> ph )
9	4, 8	wb 105	1 wff ( A. x e. A ph <-> A. x ( x e. A -> ph ) )

This definition is used by:  ralnex  2538  rexnalim  2539  dfrex2dc  2541  ralbida  2544  ralbidv2  2552  ralbid2  2554  ralbii2  2560  r2alf  2567  hbral  2579  hbra1  2580  nfra1  2581  nfraldw  2582  nfraldxy  2583  nfraldya  2585  r3al  2594  alral  2595  rsp  2597  rgen  2603  rgen2a  2604  ralim  2609  ralimi2  2610  ralimdaa  2616  ralimdv2  2620  ralrimi  2621  r19.21t  2625  ralrimd  2628  r19.21bi  2638  rexim  2644  r19.23t  2658  r19.26m  2682  r19.32r  2697  rabid2  2729  rabbi  2730  raleqf  2745  cbvralfw  2775  cbvralf  2777  cbvralvw  2790  cbvraldva2  2793  ralv  2839  ceqsralt  2849  rspct  2922  rspc  2923  rspcimdv  2930  rspc2gv  2942  ralab  2986  ralab2  2990  ralrab2  2991  reu2  3014  reu6  3015  reu3  3016  rmo4  3019  reu8  3022  rmo3f  3023  rmoim  3027  2reuswapdc  3030  2rmorex  3032  ra5  3141  rmo2ilem  3142  rmo3  3144  cbvralcsf  3210  dfss3  3236  dfss3f  3240  ssabral  3319  ss2rab  3324  rabss  3325  ssrab  3326  dfdif3  3339  ralunb  3410  reuss2  3513  rabeq0  3552  disj  3573  disj1  3575  r19.2m  3614  r19.2mOLD  3615  r19.3rm  3616  ralidm  3628  ralf0  3630  ralm  3631  ralsnsg  3746  ralsns  3747  unissb  3965  dfint2  3972  elint2  3977  elintrab  3982  ssintrab  3993  dfiin2g  4045  invdisj  4123  dftr5  4232  trint  4244  repizf2lem  4298  ordsucim  4647  ordunisuc2r  4661  setindel  4685  elirr  4688  en2lp  4701  zfregfr  4721  tfi  4729  zfinf2  4736  peano2  4742  peano5  4745  find  4746  raliunxp  4921  dmopab3  4994  issref  5170  asymref  5173  dffun7  5404  funcnv  5442  funcnvuni  5450  fnres  5500  fnopabg  5507  rexrnmpt  5851  dffo3  5855  acexmidlem2  6082  nfixpxy  6999  pw1dc0el  7218  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  fz1sbc  10503  nnwosdc  12816  isprm2  12895  istopg  15100  cbvrald  16816  decidr  16824  bdcint  16903  bdcriota  16909  bj-axempty  16919  bj-indind  16958  bj-ssom  16962  findset  16971  bj-nnord  16984  bj-inf2vn  17000  bj-inf2vn2  17001  bj-findis  17005  dfrals2  17130  alsralrex  17153  alsraln0m  17154  dfralseu2  17164