Theorem ral0 3594

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		noel 3496	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 649	. 2 ⊢ (𝑥 ∈ ∅ → 𝜑)
3	2	rgen 2583	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   ∈ wcel 2200  ∀wral 2508  ∅c0 3492

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-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2802  df-dif 3200  df-nul 3493

This theorem is referenced by:  0iin  4027  po0  4406  so0  4421  we0  4456  ord0  4486  omsinds  4718  mpt0  5457  iso0  5953  ixp0x  6890  ac6sfi  7080  fimax2gtri  7084  dcfi  7171  nnnninfeq2  7319  nninfisollem0  7320  finomni  7330  uzsinds  10696  seq3f1olemp  10767  swrd0g  11231  swrdspsleq  11238  rexfiuz  11540  fimaxre2  11778  2prm  12689  clwwlkn1  16213  bj-nntrans  16482