Theorem ral0 3611

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 3512	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 651	. 2 ⊢ (𝑥 ∈ ∅ → 𝜑)
3	2	rgen 2595	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   ∈ wcel 2203  ∀wral 2520  ∅c0 3508

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-dif 3213  df-nul 3509

This theorem is referenced by:  0iin  4050  po0  4432  so0  4447  we0  4482  ord0  4512  omsinds  4744  mpt0  5486  iso0  5990  ixp0x  6961  ac6sfi  7155  fimax2gtri  7159  dcfi  7268  nnnninfeq2  7420  nninfisollem0  7421  finomni  7431  uzsinds  10806  seq3f1olemp  10877  swrd0g  11352  swrdspsleq  11359  rexfiuz  11674  fimaxre2  11912  2prm  12824  clwwlkn1  16413  bj-nntrans  16721