Theorem rzal 3935

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 3796	. . . 4 |- ( x e. A -> A =/= (/) )
2	1	necon2bi 2704	. . 3 |- ( A = (/) -> -. x e. A )
3	2	pm2.21d 106	. 2 |- ( A = (/) -> ( x e. A -> ph ) )
4	3	ralrimiv 2879	1 |- ( A = (/) -> A. x e. A ph )

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767   A.wral 2817   (/)c0 3790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-v 3120  df-dif 3484  df-nul 3791

This theorem is referenced by:  ralidm  3937  rgenz  3939  ralf0  3940  raaan  3941  raaanv  3942  iinrab2  4394  riinrab  4407  reusv2lem2  4655  cnvpo  5551  dffi3  7903  brdom3  8918  dedekind  9755  fimaxre2  10503  efgs1  16626  opnnei  19489  axcontlem12  24101  ubthlem1  25609  nofulllem2  29390  mbfresfi  29988  bddiblnc  30012  blbnd  30210  rrnequiv  30258  upbdrech2  31408  stoweidlem9  31632  fourierdlem31  31761  raaan2  31970