Theorem rzal 3870

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 3736	. . . 4 |- ( x e. A -> A =/= (/) )
2	1	necon2bi 2653	. . 3 |- ( A = (/) -> -. x e. A )
3	2	pm2.21d 110	. 2 |- ( A = (/) -> ( x e. A -> ph ) )
4	3	ralrimiv 2799	1 |- ( A = (/) -> A. x e. A ph )

Syntax hints:   -> wi 4   = wceq 1443   e. wcel 1886   A.wral 2736   (/)c0 3730

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-v 3046  df-dif 3406  df-nul 3731

This theorem is referenced by:  ralidm  3872  rgenz  3874  ralf0  3875  raaan  3876  raaanv  3877  iinrab2  4340  riinrab  4353  reusv2lem2  4604  cnvpo  5373  dffi3  7942  brdom3  8953  dedekind  9794  fimaxre2  10549  efgs1  17378  opnnei  20129  axcontlem12  24998  ubthlem1  26505  nofulllem2  30585  mbfresfi  31980  bddiblnc  32005  blbnd  32112  rrnequiv  32160  upbdrech2  37520  stoweidlem9  37863  fourierdlem31  37994  fourierdlem31OLD  37995  raaan2  38590  nbgr0edg  39408  0vtxrgr  39575