Theorem rzal 3779

Description: Vacuous quantification is always true. (Contributed by NM, 11-Mar-1997.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
rzal	|- ( A = (/) -> A. x e. A ph )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem rzal

Step	Hyp	Ref	Expression
1		ne0i 3641	. . . 4 |- ( x e. A -> A =/= (/) )
2	1	necon2bi 2655	. . 3 |- ( A = (/) -> -. x e. A )
3	2	pm2.21d 106	. 2 |- ( A = (/) -> ( x e. A -> ph ) )
4	3	ralrimiv 2796	1 |- ( A = (/) -> A. x e. A ph )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   A.wral 2713   (/)c0 3635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-v 2972  df-dif 3329  df-nul 3636

This theorem is referenced by:  ralidm  3781  rgenz  3783  ralf0  3784  raaan  3785  raaanv  3786  iinrab2  4231  riinrab  4244  reusv2lem2  4492  cnvpo  5373  dffi3  7679  brdom3  8693  dedekind  9531  fimaxre2  10276  efgs1  16230  opnnei  18722  axcontlem12  23219  ubthlem1  24269  nofulllem2  27842  mbfresfi  28435  bddiblnc  28459  blbnd  28683  rrnequiv  28731  stoweidlem9  29801  raaan2  29996