Theorem bj-omind 10729

Description: om is an inductive class. (Contributed by BJ, 30-Nov-2019.)

Assertion

Ref	Expression
bj-omind	|- Ind om

Proof of Theorem bj-omind

Step	Hyp	Ref	Expression
1		bj-indint 10726	. 2 |- Ind |^| { x e. _V | Ind x }
2		bj-dfom 10728	. . . 4 |- om = |^| { x | Ind x }
3		rabab 2620	. . . . 5 |- { x e. _V | Ind x } = { x | Ind x }
4	3	inteqi 3640	. . . 4 |- |^| { x e. _V | Ind x } = |^| { x | Ind x }
5	2, 4	eqtr4i 2104	. . 3 |- om = |^| { x e. _V | Ind x }
6		bj-indeq 10724	. . 3 |- ( om = |^| { x e. _V | Ind x } -> (Ind om <-> Ind |^| { x e. _V | Ind x } ) )
7	5, 6	ax-mp 7	. 2 |- (Ind om <-> Ind |^| { x e. _V | Ind x } )
8	1, 7	mpbir 144	1 |- Ind om

Syntax hints:   <-> wb 103   = wceq 1284   {cab 2067   {crab 2352   _Vcvv 2601   |^|cint 3636   omcom 4331  Ind wind 10721

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-nul 3904  ax-pr 3964  ax-un 4188  ax-bd0 10604  ax-bdor 10607  ax-bdex 10610  ax-bdeq 10611  ax-bdel 10612  ax-bdsb 10613  ax-bdsep 10675

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-rab 2357  df-v 2603  df-dif 2975  df-un 2977  df-nul 3252  df-sn 3404  df-pr 3405  df-uni 3602  df-int 3637  df-suc 4126  df-iom 4332  df-bdc 10632  df-bj-ind 10722

This theorem is referenced by:  bj-om  10732  bj-peano2  10734  peano5set  10735