Theorem rzal 4073

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 3921	. . . 4 |- ( x e. A -> A =/= (/) )
2	1	necon2bi 2824	. . 3 |- ( A = (/) -> -. x e. A )
3	2	pm2.21d 118	. 2 |- ( A = (/) -> ( x e. A -> ph ) )
4	3	ralrimiv 2965	1 |- ( A = (/) -> A. x e. A ph )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   A.wral 2912   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  ralidm  4075  rgenzOLD  4077  ralf0OLD  4079  raaan  4082  iinrab2  4583  riinrab  4596  reusv2lem2  4869  reusv2lem2OLD  4870  cnvpo  5673  dffi3  8337  brdom3  9350  dedekind  10200  fimaxre2  10969  mgm0  17255  sgrp0  17291  efgs1  18148  opnnei  20924  axcontlem12  25855  nbgr0edg  26253  cplgr0v  26323  0vtxrgr  26472  0vconngr  27053  frgr1v  27135  ubthlem1  27726  matunitlindf  33407  mbfresfi  33456  bddiblnc  33480  blbnd  33586  rrnequiv  33634  upbdrech2  39522  fiminre2  39594  limsupubuz  39945  stoweidlem9  40226  fourierdlem31  40355  raaan2  41175