Theorem ralrn 7022

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013.) (Revised by Mario Carneiro, 20-Aug-2014.)

Hypothesis

Ref	Expression
rexrn.1	⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrn	⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem ralrn

Step	Hyp	Ref	Expression
1		fvexd 6837	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ V)
2		fvelrnb 6883	. . 3 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥))
3		eqcom 2736	. . . 4 ⊢ ((𝐹‘𝑦) = 𝑥 ↔ 𝑥 = (𝐹‘𝑦))
4	3	rexbii 3076	. . 3 ⊢ (∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = 𝑥 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦))
5	2, 4	bitrdi 287	. 2 ⊢ (𝐹 Fn 𝐴 → (𝑥 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝐴 𝑥 = (𝐹‘𝑦)))
6		rexrn.1	. . 3 ⊢ (𝑥 = (𝐹‘𝑦) → (𝜑 ↔ 𝜓))
7	6	adantl 481	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 = (𝐹‘𝑦)) → (𝜑 ↔ 𝜓))
8	1, 5, 7	ralxfr2d 5349	1 ⊢ (𝐹 Fn 𝐴 → (∀𝑥 ∈ ran 𝐹𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053  Vcvv 3436  ran crn 5620   Fn wfn 6477  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490

This theorem is referenced by:  ralrnmptw  7028  ralrnmpt  7030  cbvfo  7226  isoselem  7278  indexfi  9250  ordtypelem9  9418  ordtypelem10  9419  wemapwe  9593  numacn  9943  acndom  9945  rpnnen1lem3  12880  fsequb2  13883  limsuple  15385  limsupval2  15387  climsup  15577  ruclem11  16149  ruclem12  16150  prmreclem6  16833  imasaddfnlem  17432  imasvscafn  17441  cycsubgcl  19085  ghmrn  19108  ghmnsgima  19119  pgpssslw  19493  gexex  19732  dprdfcntz  19896  znf1o  21458  frlmlbs  21704  lindfrn  21728  ptcnplem  23506  kqt0lem  23621  isr0  23622  regr1lem2  23625  uzrest  23782  tmdgsum2  23981  imasf1oxmet  24261  imasf1omet  24262  bndth  24855  evth  24856  ovolficcss  25368  ovollb2lem  25387  ovolunlem1  25396  ovoliunlem1  25401  ovoliunlem2  25402  ovoliun2  25405  ovolscalem1  25412  ovolicc1  25415  voliunlem2  25450  voliunlem3  25451  ioombl1lem4  25460  uniioovol  25478  uniioombllem2  25482  uniioombllem3  25484  uniioombllem6  25487  volsup2  25504  vitalilem3  25509  mbfsup  25563  mbfinf  25564  mbflimsup  25565  itg1ge0  25585  itg1mulc  25603  itg1climres  25613  mbfi1fseqlem4  25617  itg2seq  25641  itg2monolem1  25649  itg2mono  25652  itg2i1fseq2  25655  itg2gt0  25659  itg2cnlem1  25660  itg2cn  25662  limciun  25793  plycpn  26195  hmopidmchi  32095  hmopidmpji  32096  rge0scvg  33922  mclsax  35552  mblfinlem2  37648  ismtyhmeolem  37794  nacsfix  42695  fnwe2lem2  43034  gneispace  44117  climinf  45597  liminfval2  45759