Theorem dfrex2 2116

Description: Relationship between restricted universal and existential quantifiers.

Assertion

Ref	Expression
dfrex2	|- (E.x e. A ph <-> -. A.x e. A -. ph)

Proof of Theorem dfrex2

Step	Hyp	Ref	Expression
1		ralnex 2113	. 2 |- (A.x e. A -. ph <-> -. E.x e. A ph)
2	1	con2bii 238	1 |- (E.x e. A ph <-> -. A.x e. A -. ph)

Syntax hints:  -. wn 2   <-> wb 163  A.wral 2105  E.wrex 2106

This theorem is referenced by:  r19.35 2231  sbcrext 2528  sbcrexgf 2530  r19.9rzv 2963  rexpr 3082  rexxfrd 3838  rexxfr 3841  rexxp 4042  rexxpf 4044  cbvexfo 4862  tz7.49 5168  abianfp 5171  supnub 5672  zfregs2 5755  ac6n 5919  alephval3 6051  ssxrOLD 6715  supxrre 7292  infxpidmlem12 8832  lpbl 9157  chpssati 11935  chrelat3 11943  4nprm 13781  r19.30 13817  dffr5 13831  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  fdc 15812  zfregs2VD 16665  hlrelat1 17049

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain