Theorem 19.42v 1775

Description: Version of 19.42 1972 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
19.42v

Distinct variable group:   ,

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		19.41v 1771	. 2
2		exancom 1671	. 2
3		ancom 450	. 2
4	1, 2, 3	3bitr4i 277	1

Syntax hints:  <->wb 184  /\wa 369  E.wex 1612

This theorem is referenced by:  exdistr  1776  19.42vv  1777  19.42vvv  1778  4exdistr  1781  eeeanv  1989  cbvex2OLD  2029  2sb5  2187  rexcom4a  3130  ceqsex2  3147  reuind  3303  2reu5lem3  3307  sbccomlem  3406  bm1.3ii  4576  eqvinop  4736  dmopabss  5219  dmopab3  5220  mptpreima  5505  brprcneu  5864  fndmin  5994  fliftf  6213  dfoprab2  6343  dmoprab  6383  dmoprabss  6384  fnoprabg  6403  uniuni  6609  zfrep6  6768  opabex3d  6778  opabex3  6779  fsplit  6905  eroveu  7425  rankuni  8302  aceq1  8519  dfac3  8523  kmlem14  8564  kmlem15  8565  axdc2lem  8849  1idpr  9428  ltexprlem1  9435  ltexprlem4  9438  shftdm  12904  joindm  15633  meetdm  15647  ntreq0  19578  cnextf  20566  usg2spot2nb  25065  adjeu  26808  rexunirn  27390  mptfnf  27499  fpwrelmapffslem  27555  dfiota3  29573  brimg  29587  funpartlem  29592  itg2addnc  30069  sbccom2lem  30529  pm11.58  31296  pm11.71  31303  2sbc5g  31323  iotasbc2  31327  stoweidlem60  31842  ax6e2nd  33331  ax6e2ndVD  33708  ax6e2ndALT  33730  bnj1019  33838  bnj1209  33855  bnj1033  34025  bnj1189  34065  bj-eeanvw  34267  bj-rexcom4  34445  bj-rexcom4a  34446  bj-snsetex  34521  bj-snglc  34527  rp-isfinite6  37744  elintima  37765  xpcogend  37773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613