Theorem ral0 2410

Description: Vacuous universal quantification is always true.

Assertion

Ref	Expression
ral0	⊢ ∀x ∈ ∅ φ

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		noel 2335	. . 3 ⊢ ¬ x ∈ ∅
2	1	pm2.21i 80	. 2 ⊢ (x ∈ ∅ → φ)
3	2	rgen 1745	1 ⊢ ∀x ∈ ∅ φ

Syntax hints:   ∈ wcel 999  ∀wral 1692  ∅c0 2331

This theorem is referenced by:  0iin 2660  ixp0x 4420  xrsupsslem 6158  xrinfmsslem 6159  xrsup0 6179  0met 7910  chocnul 9375  emhgrat 10859

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-ral 1696  df-v 1859  df-dif 2100  df-nul 2332

Copyright terms: Public domain