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	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

Detailed syntax breakdown of Definition df-ral

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		cA	. . 3 class 𝐴
4	1, 2, 3	wral 2528	. 2 wff ∀𝑥 ∈ 𝐴 𝜑
5	2	cv 1401	. . . . 5 class 𝑥
6	5, 3	wcel 2209	. . . 4 wff 𝑥 ∈ 𝐴
7	6, 1	wi 4	. . 3 wff (𝑥 ∈ 𝐴 → 𝜑)
8	7, 2	wal 1400	. 2 wff ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
9	4, 8	wb 105	1 wff (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))

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  4234  trint  4246  repizf2lem  4300  ordsucim  4649  ordunisuc2r  4663  setindel  4687  elirr  4690  en2lp  4703  zfregfr  4723  tfi  4731  zfinf2  4738  peano2  4744  peano5  4747  find  4748  raliunxp  4923  dmopab3  4996  issref  5173  asymref  5176  dffun7  5407  funcnv  5445  funcnvuni  5453  fnres  5503  fnopabg  5510  rexrnmpt  5854  dffo3  5858  acexmidlem2  6085  nfixpxy  7003  pw1dc0el  7222  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  fz1sbc  10520  nnwosdc  12841  isprm2  12920  istopg  15225  cbvrald  17021  decidr  17029  bdcint  17108  bdcriota  17114  bj-axempty  17124  bj-indind  17163  bj-ssom  17167  findset  17176  bj-nnord  17189  bj-inf2vn  17205  bj-inf2vn2  17206  bj-findis  17210  dfrals2  17337  alsralrex  17360  alsraln0m  17361  dfralseu2  17371